Theorem syl7 26

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

Syntax hints:   -> wi 3

This theorem is referenced by:  syl7ib 233  syl3an3 1132  ee13 1275  hbae 1505  ax11 1589  a12study 1769  vtoclegft 2356  uniiunlem 2693  tz7.7 3684  f1oweALT 4883  nneneq 5606  r1ord 5766  ltbtwnpq 6236  nnunb 7279  iscms2lem5 9271  findcardOLD 10179  atcvat4i 11969  mdsymlem5 11979  sumdmdii 11987  ndvdssub 13710  dfon2lem6 13854  wfrlem12 13968  unpde2eg2 14406  lvsovso 15038  icmpmon 15165  cnpfillim 15589  fmfnfmlem4 15597  erdisj3 16266  cvrat4 17076

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

Copyright terms: Public domain