Theorem syl7 24

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

Hypotheses

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

Assertion

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

Proof of Theorem syl7

Step	Hyp	Ref	Expression
1		syl7.1	. 2 |- (ph -> (ps -> (ch -> th)))
2		syl7.2	. . 3 |- (ta -> ch)
3	2	syl4 19	. 2 |- ((ch -> th) -> (ta -> th))
4	1, 3	syl6 23	1 |- (ph -> (ps -> (ta -> th)))

Syntax hints:   -> wi 2

This theorem is referenced by:  bisyl7 189  syl3an3 621  eq5 824  tz7.7 2224  fvopab2 2878  f1oweOLD 2944  tz7.49 2997  nneneq 3408  r1ord 3499  ltbtwnpq 3878  nnunb 4520  atcvat4 5775  mdsymlem5 5780  sumdmdi 5785

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

metamath.org