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  234  syl3an3  1303  hbae  2149  tz7.7  5449  fvmptt  5965  f1oweALT  6777  wfrlem12  7047  nneneq  7755  pr2nelem  8435  cfcoflem  8702  nnunb  10865  ndvdssub  14388  lsmcv  18364  gsummoncoe1  18898  uvcendim  19405  2ndcsep  20474  atcvat4i  28050  mdsymlem5  28060  sumdmdii  28068  dfon2lem6  30434  frrlem11  30526  colineardim1  30828  bj-hbaeb2  31420  wl-ax12  31913  hbae-o  32473  ax12  32475  cvrat4  33008  llncvrlpln2  33122  lplncvrlvol2  33180  dihmeetlem3N  34873  eel2122old  37103