Theorem pm2.36 91

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

Assertion

Ref	Expression
pm2.36	|- ((ps -> ch) -> ((-. ph -> ps) -> (-. ch -> ph)))

Proof of Theorem pm2.36

Step	Hyp	Ref	Expression
1		syl1 16	. 2 |- ((ps -> ch) -> ((-. ph -> ps) -> (-. ph -> ch)))
2		con1 84	. 2 |- ((-. ph -> ch) -> (-. ch -> ph))
3	1, 2	syl6 23	1 |- ((ps -> ch) -> ((-. ph -> ps) -> (-. ch -> ph)))

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