Theorem syl7 23

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	imim1i 16	. 2 |- ((ch -> th) -> (ta -> th))
4	1, 3	syl6 22	1 |- (ph -> (ps -> (ta -> th)))

Syntax hints:   -> wi 3

This theorem is referenced by:  syl7ib 216  syl3an3 861  hbae 1145  ax11 1219  a12study 1378  uniiunlem 2132  tz7.7 2973  f1oweALT 3906  nneneq 4512  r1ord 4655  ltbtwnpq 5084  nnunb 6070  iscms2lem5 7993  atcvat4 10324  mdsymlem5 10334  sumdmdi 10342  icmpmon 10744

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

Copyright terms: Public domain