Theorem pm2.36 91

Description: Theorem *2.36 of [WhiteheadRussell] p. 105.

Assertion

Ref	Expression
pm2.36	⊢ ((ψ → χ) → ((¬ φ → ψ) → (¬ χ → φ)))

Proof of Theorem pm2.36

Step	Hyp	Ref	Expression
1		syl1 16	. 2 ⊢ ((ψ → χ) → ((¬ φ → ψ) → (¬ φ → χ)))
2		con1 84	. 2 ⊢ ((¬ φ → χ) → (¬ χ → φ))
3	1, 2	syl6 23	1 ⊢ ((ψ → χ) → ((¬ φ → ψ) → (¬ χ → φ)))

Syntax hints:  ¬ wn 1   → wi 2

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

metamath.org