1 p => q Premise 2 q => r Assumption 3 p Assumption 4 q Implication Elimination 1 3 5 r Implication Elimination 2 4 6 p => r Implication Introduction 3 5 7 (q => r) => (p => r) Implication Introduction 2 6 1 q => r Premise 2 p => q Assumption 3 p Assumption 4 q Implication Elimination 2 3 5 r Implication Elimination 1 4 6 p => r Implication Introduction 3 5 7 (p => q) => (p => r) Implication Introduction 2 6 1 p => (q => r) Premise 2 q Assumption 3 p Assumption 4 q => r Implication Elimination 1 3 5 r Implication Elimination 4 2 6 p => r Implication Introduction 3 5 7 q => (p => r) Implication Introduction 2 6 1 p => (q => r) Premise 2 p => q Premise 3 p Assumption 4 q => r Implication Elimination 1 3 5 q Implication Elimination 2 3 6 r Implication Elimination 4 5 7 p => r Implication Introduction 3 6 1 ~p => r Premise 2 ~(p | r) Assumption 3 p Assumption 4 p | r Or Introduction 3 5 p => p | r Implication Introduction 3 4 6 p Assumption 7 ~(p | r) Reiteration 2 8 p => ~(p | r) Implication Introduction 6 7 9 ~p Negation Introduction 5 8 10 r Implication Elimination 1 9 11 p | r Or Introduction 10 12 ~(p | r) => p | r Implication Introduction 2 11 13 ~(p | r) Assumption 14 ~(p | r) => ~(p | r) Implication Introduction 13 13 15 ~~(p | r) Negation Introduction 12 14 16 p | r Negation Elimination 15 1 p Premise 2 q Assumption 3 p Reiteration 1 4 q => p Implication Introduction 2 3 1 p => (q => r) Premise 2 p => q Assumption 3 p Assumption 4 q Implication Elimination 2 3 5 q => r Implication Elimination 1 3 6 r Implication Elimination 5 4 7 p => r Implication Introduction 3 6 8 (p => q) => (p => r) Implication Introduction 2 7 1 ~q => ~p Premise 2 p Assumption 3 ~q Assumption 4 p Reiteration 2 5 ~q => p Implication Introduction 3 4 6 ~~q Negation Introduction 5 1 7 q Negation Elimination 6 8 p => q Implication Introduction 2 7 1 p Premise 2 ~p Premise 3 ~q Assumption 4 p Reiteration 1 5 ~q => p Implication Introduction 3 4 6 ~q Assumption 7 ~p Reiteration 2 8 ~q => ~p Implication Introduction 6 7 9 ~~q Negation Introduction 5 8 10 q Negation Elimination 9 1 p => q Premise 2 ~q Premise 3 p Assumption 4 ~q Reiteration 2 5 p => ~q Implication Introduction 3 4 6 ~p Negation Introduction 1 5