Theorem syl5 32

Description: A syllogism rule of inference. The second premise is used to replace the second antecedent of the first premise. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 25-May-2013.)

Hypotheses

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

Assertion

Ref	Expression
syl5	|- ( ch -> ( ph -> th ) )

Proof of Theorem syl5

Step	Hyp	Ref	Expression
1		syl5.1	. . 3 |- ( ph -> ps )
2		syl5.2	. . 3 |- ( ch -> ( ps -> th ) )
3	1, 2	syl5com 29	. 2 |- ( ph -> ( ch -> th ) )
4	3	com12 30	1 |- ( ch -> ( ph -> th ) )

Syntax hints:   -> wi 4

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

This theorem is referenced by:  syl56  34  syl2im  38  imim12i  59  pm2.86d  99  syl5bi  151  syl5bir  152  syl5ib  153  adantld  276  adantrd  277  impel  278  mpan9  279  nsyli  644  pm2.36  799  pm4.72  822  pm2.18dc  850  con1dc  851  jadc  858  pm2.521dcALT  865  con1biimdc  868  condandc  876  pm5.18dc  878  pm2.68dc  889  annimdc  932  syl3an2  1267  syl2an23an  1294  xor3dc  1382  alrimdh  1472  spsd  1531  a5i  1536  19.21h  1550  hbnt  1646  hbae  1711  sbiedh  1780  exdistrfor  1793  sbcof2  1803  ax11a2  1814  ax11v  1820  sb4  1825  hbsb4t  2006  exmoeudc  2082  euimmo  2086  mopick  2097  r19.37  2622  spcimgft  2806  spcimegft  2808  rr19.28v  2870  mob2  2910  euind  2917  reuind  2935  sbeqalb  3011  triun  4100  csbexga  4117  copsexg  4229  trssord  4365  trsuc  4407  trsucss  4408  abnexg  4431  ralxfrd  4447  rexxfrd  4448  ralxfrALT  4452  sucprcreg  4533  nlimsucg  4550  tfis  4567  relssres  4929  issref  4993  dmsnopg  5082  dfco2a  5111  imadif  5278  fvelima  5548  mptfvex  5581  fvmptdf  5583  fvmptf  5588  funfvima2  5728  funfvima3  5729  foco2  5733  isores3  5794  oprabid  5885  ovmpt4g  5975  ovmpos  5976  ov2gf  5977  ovmpodf  5984  suppssfv  6057  suppssov1  6058  fo2ndf  6206  rntpos  6236  tposf2  6247  nnmordi  6495  nnmord  6496  nnaordex  6507  ectocld  6579  qsel  6590  mapsn  6668  f1oeng  6735  mapen  6824  nneneq  6835  findcard2  6867  findcard2s  6868  ac6sfi  6876  fiintim  6906  sbthlem1  6934  pr2ne  7169  ltbtwnnqq  7377  prnmaddl  7452  genpcdl  7481  genpcuu  7482  ltaddpr  7559  lteupri  7579  recexprlemss1l  7597  recexprlemss1u  7598  cauappcvgprlemdisj  7613  lttrsr  7724  recexgt0sr  7735  mulgt0sr  7740  axprecex  7842  rereceu  7851  addlsub  8289  recexap  8571  0mnnnnn0  9167  prime  9311  zeo  9317  fnn0ind  9328  zindd  9330  btwnz  9331  lbzbi  9575  addmodlteq  10354  facwordi  10674  seq3coll  10777  qdenre  11166  climcau  11310  serf0  11315  zsumdc  11347  fsum2dlemstep  11397  fsum2d  11398  fsumabs  11428  fsumiun  11440  zproddc  11542  fprod2dlemstep  11585  fprod2d  11586  odd2np1  11832  ndvdssub  11889  dfgcd2  11969  nprm  12077  rpexp  12107  pc2dvds  12283  pcfac  12302  lmss  13040  lmtopcnp  13044  txcn  13069  txlm  13073  xmettri2  13155  blin2  13226  metcnp3  13305  limcresi  13429  logbgcd1irr  13679  lgsdir2lem2  13724  lgsne0  13733  2sqlem6  13750  2sqlem10  13755  bj-stim  13781  bj-stan  13782  bj-stand  13783  bj-stal  13784  bj-sbimedh  13806  bj-vtoclgft  13810  elabgft1  13813  elabgf2  13815