Theorem syl8 25

Description: A syllogism rule of inference. The second premise is used to replace the consequent of the first premise.

Hypotheses

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

Assertion

Ref	Expression
syl8	|- (ph -> (ps -> (ch -> ta )))

Proof of Theorem syl8

Step	Hyp	Ref	Expression
1		syl8.1	. 2 |- (ph -> (ps -> (ch -> th)))
2		syl8.2	. . 3 |- (th -> ta )
3	2	syl3 18	. 2 |- ((ch -> th) -> (ch -> ta ))
4	1, 3	syl6 23	1 |- (ph -> (ps -> (ch -> ta )))

Syntax hints:   -> wi 2

This theorem is referenced by:  bisyl8 190  onfr 2237  ssorduni 2249  findsg 2398  tfindsg 2402  tfrlem2 2950  tz7.49 2997  nneneq 3408  aceq6b 3565  ltbtwnpq 3878  reclem3pr 3952  suppsr2 4017  qrecclt 4646  elspansn5t 5479  sumdmd 5787

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

metamath.org