Theorem syl7 70

Description: A syllogism rule of inference. The first premise is used to replace the third antecedent of the second premise. (Contributed by NM, 12-Jan-1993.) (Proof shortened by Wolf Lammen, 3-Aug-2012.)

Hypotheses

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

Assertion

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

Proof of Theorem syl7

Step	Hyp	Ref	Expression
1		syl7.1	. . 3 |- ( ph -> ps )
2	1	a1i 11	. 2 |- ( ch -> ( ph -> ps ) )
3		syl7.2	. 2 |- ( ch -> ( th -> ( ps -> ta ) ) )
4	2, 3	syl5d 69	1 |- ( ch -> ( th -> ( ph -> ta ) ) )

Syntax hints:   -> wi 4

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

This theorem is referenced by:  syl7bi  233  syl3an3  1299  hbae  2110  tz7.7  5464  fvmptt  5977  f1oweALT  6787  wfrlem12  7051  nneneq  7757  pr2nelem  8436  cfcoflem  8702  nnunb  10865  ndvdssub  14375  lsmcv  18351  gsummoncoe1  18885  uvcendim  19391  2ndcsep  20460  atcvat4i  28035  mdsymlem5  28045  sumdmdii  28053  dfon2lem6  30428  frrlem11  30520  colineardim1  30820  bj-hbaeb2  31377  wl-ax12  31826  hbae-o  32391  ax12  32393  cvrat4  32926  llncvrlpln2  33040  lplncvrlvol2  33098  dihmeetlem3N  34791  eel2122old  36963