Theorem syl7 63

Description: A syllogism rule of inference. The first premise is used to replace the third antecedent of the second premise. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 3-Aug-2012.)

Hypotheses

Ref	Expression
syl7.1	|- (ph -> ps)
syl7.2	|- (ch -> (th -> (ps -> ta)))

Assertion

Ref	Expression
syl7	|- (ch -> (th -> (ph -> ta)))

Proof of Theorem syl7

Step	Hyp	Ref	Expression
1		syl7.1	. . 3 |- (ph -> ps)
2	1	a1i 10	. 2 |- (ch -> (ph -> ps))
3		syl7.2	. 2 |- (ch -> (th -> (ps -> ta)))
4	2, 3	syl5d 62	1 |- (ch -> (th -> (ph -> ta)))

Syntax hints:   -> wi 4

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

This theorem is referenced by:  syl7bi  221  syl3an3  1217  ax10lem4  1941  hbae  1953  hbae-o  2153  ax11  2155  sfinltfin  4536