Theorem syl1 16

Description: A closed form of syllogism. Theorem *2.05 of [WhiteheadRussell] p. 100.

Assertion

Ref	Expression
syl1	|- ((ph -> ps) -> ((ch -> ph) -> (ch -> ps)))

Proof of Theorem syl1

Step	Hyp	Ref	Expression
1		ax-1 3	. 2 |- ((ph -> ps) -> (ch -> (ph -> ps)))
2	1	a2d 15	1 |- ((ph -> ps) -> ((ch -> ph) -> (ch -> ps)))

Syntax hints:   -> wi 2

This theorem is referenced by:  syl2 17  syldd 50  pm2.36 91  pm2.61 109  osumlem4 5533

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

metamath.org