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 859  hbae 1141  ax11 1214  a12study 1371  uniiunlem 2122  tz7.7 2963  f1oweALT 3891  nneneq 4492  r1ord 4627  ltbtwnpq 5056  nnunb 6017  iscms2lem5 7927  atcvat4 10232  mdsymlem5 10242  sumdmdi 10249  icmpmon 10587

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

Copyright terms: Public domain