Hilbert Library

1 p => r Premise 2 r => (q => r) Implication Creation 3 (r => (q => r)) => (p => (r => (q => r))) Implication Creation 4 p => (r => (q => r)) Implication Elimination 3 2 5 (p => (r => (q => r))) => ((p => r) => (p => (q => r))) Implication Distribution 6 (p => r) => (p => (q => r)) Implication Elimination 5 4 7 p => (q => r) Implication Elimination 6 1 1 (~q => ~p) => (p => q) Implication Reversal 2 ((~q => ~p) => (p => q)) => (~p => ((~q => ~p) => (p => q))) Implication Creation 3 ~p => ((~q => ~p) => (p => q)) Implication Elimination 2 1 4 (~p => ((~q => ~p) => (p => q))) => ((~p => (~q => ~p)) => (~p => (p => q))) Implication Distribution 5 (~p => (~q => ~p)) => (~p => (p => q)) Implication Elimination 4 3 6 ~p => (~q => ~p) Implication Creation 7 ~p => (p => q) Implication Elimination 5 6 1 p => q Premise 2 (q => r) => (p => (q => r)) Implication Creation Schema 3 (p => (q => r)) => ((p => q) => (p => r)) Implication Distribution Schema 4 (q => r) => ((p => q) => (p => r)) Transitivity 2 3 5 (p => q) => ((q => r) => (p => q)) Implication Creation Schema 6 (q => r) => (p => q) Implication Elimination 5 1 7 (q => r) => (p => r) Conditional Deduction 4 6 1 q => r Premise 2 p => (q => r) Implication Creation 1 3 (p => q) => (p => r) Implication Distribution 2 1 p => (q => r) Premise 2 (p => (q => r)) => (q => (p => (q => r))) Implication Creation Schema 3 q => (p => (q => r)) Implication Elimination 2 1 4 (p => (q => r)) => ((p => q) => (p => r)) Implication Distribution Schema 5 ((p => (q => r)) => ((p => q) => (p => r))) => (q => ((p => (q => r)) => ((p => q) => (p => r)))) Implication Creation Schema 6 q => ((p => (q => r)) => ((p => q) => (p => r))) Implication Elimination 5 4 7 q => ((p => q) => (p => r)) Conditional Deduction 3 6 8 (q => ((p => q) => (p => r))) => ((q => (p => q)) => (q => (p => r))) Implication Distribution Schema 9 (q => (p => q)) => (q => (p => r)) Implication Elimination 8 7 10 q => (p => q) Implication Creation Schema 11 q => (p => r) Implication Elimination 9 10 1 p => (q => r) Premise 2 p => q Premise 3 (p => q) => (p => r) Implication Distribution 1 4 p => r Implication Elimination 3 2 1 p => r Premise 2 q => ~r Premise 3 ~~q => q Negation Elimination Schema 4 ~~q => (q => ~r) Implication Creation 2 5 (~~q => q) => (~~q => ~r) Implication Distribution 4 6 ~~q => ~r Implication Elimination 5 3 7 r => ~q Implication Reversal 6 8 p => (r => ~q) Implication Creation 7 9 (p => r) => (p => ~q) Implication Distribution 8 10 p => ~q Implication Elimination 9 1 1 p => q Premise 2 p => ~q Premise 3 p => ~p Contradiction 1 2 4 ~p Implication Reduction 3 1 p => q Premise 2 q => ~~q Negation Introduction Schema 3 p => ~~q Transitivity 1 2 4 ~q => ~q Identity Schema 5 ~q => ~p Contradiction 4 3 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 1 p Premise 2 p => (q => p) Implication Creation Schema 3 q => p Implication Elimination 2 1 1 p => (q => r) Premise 2 (p => (q => r)) => ((p => q) => (p => r)) Implication Distribution Schema 3 (p => q) => (p => r) Implication Elimination 2 1 1 p => ~p Premise 2 p => (~p => ~(p => ~p)) Inconsistency 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 => ~p) Implication Elimination 4 1 6 ~~(p => ~p) => ~p Contrapositive 5 7 (p => ~p) => ~~(p => ~p) Negation Introduction Schema 8 (p => ~p) => ~p Transitivity 6 7 9 ~p Implication Elimination 8 1 1 ~q => ~p Premise 2 (~q => ~p) => (p => q) Implication Reversal Schema 3 p => q Implication Elimination 2 1 1 p Premise 2 ~p Premise 3 ~q => ~p Implication Creation 2 4 p => q Implication Reversal 3 5 q Implication Elimination 4 1 1 (~q => ~p) => (p => q) Implication Reversal Schema 2 ((~q => ~p) => (p => q)) => (~p => ((~q => ~p) => (p => q))) Implication Creation Schema 3 ~p => ((~q => ~p) => (p => q)) Implication Elimination 2 1 4 (~p => ((~q => ~p) => (p => q))) => ((~p => (~q => ~p)) => (~p => (p => q))) Implication Distribution Schema 5 (~p => (~q => ~p)) => (~p => (p => q)) Implication Elimination 4 3 6 ~p => (~q => ~p) Implication Creation Schema 7 ~p => (p => q) Implication Elimination 5 6 1 p => q Premise 2 ~q Premise 3 ~q => ~p Contrapositive 1 4 ~p Implication Elimination 3 2 1 ~~p Premise 2 ~~~~p => ~~p Implication Creation 1 3 ~p => ~~~p Implication Reversal 2 4 ~~p => p Implication Reversal 3 5 p Implication Elimination 4 1 1 ~~p => (~~~~p => ~~p) Implication Creation Schema 2 (~~~~p => ~~p) => (~p => ~~~p) Implication Reversal Schema 3 ~~p => (~p => ~~~p) Transitivity 1 2 4 (~p => ~~~p) => (~~p => p) Implication Reversal Schema 5 ~~p => (~~p => p) Transitivity 3 4 6 (~~p => (~~p => p)) => ((~~p => ~~p) => (~~p => p)) Implication Distribution Schema 7 (~~p => ~~p) => (~~p => p) Implication Elimination 6 5 8 ~~p => ~~p Identity Schema 9 ~~p => p Implication Elimination 7 8 1 p Premise 2 ~~~p => ~p Negation Elimination Schema 3 p => ~~p Implication Reversal 2 4 ~~p Implication Elimination 3 1 1 ~~~p => ~p Negation Elimination Schema 2 (~~~p => ~p) => (p => ~~p) Implication Reversal Schema 3 p => ~~p Implication Elimination 2 1 1 p => q Premise 2 q => r Premise 3 p => (q => r) Implication Creation 2 4 (p => q) => (p => r) Implication Distribution 3 5 p => r Implication Elimination 4 1