1 p => (p => p) Implication Creation Schema 2 p => ((p => p) => p) Implication Creation Schema 3 (p => ((p => p) => p)) => ((p => (p => p)) => (p => p)) Implication Distribution Schema 4 (p => (p => p)) => (p => p) Implication Elimination 3 2 5 p => p Implication Elimination 4 1