Theorem sylOLD 13

Description: An inference version of the transitive laws for implication.

Hypotheses

Ref	Expression
syl.1	|- (ph -> ps)
syl.2	|- (ps -> ch)

Assertion

Ref	Expression
sylOLD	|- (ph -> ch)

Proof of Theorem sylOLD

Step	Hyp	Ref	Expression
1		syl.1	. 2 |- (ph -> ps)
2		syl.2	. . . 4 |- (ps -> ch)
3	2	a1i 8	. . 3 |- (ph -> (ps -> ch))
4	3	a2i 10	. 2 |- ((ph -> ps) -> (ph -> ch))
5	1, 4	ax-mp 7	1 |- (ph -> ch)

Syntax hints:   -> wi 3

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

Copyright terms: Public domain