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  639  pm2.36  794  pm4.72  817  pm2.18dc  845  con1dc  846  jadc  853  pm2.521dcALT  860  con1biimdc  863  condandc  871  pm5.18dc  873  pm2.68dc  884  annimdc  927  syl3an2  1262  syl2an23an  1289  xor3dc  1377  alrimdh  1467  spsd  1526  a5i  1531  19.21h  1545  hbnt  1641  hbae  1706  sbiedh  1775  exdistrfor  1788  sbcof2  1798  ax11a2  1809  ax11v  1815  sb4  1820  hbsb4t  2001  exmoeudc  2077  euimmo  2081  mopick  2092  r19.37  2618  spcimgft  2802  spcimegft  2804  rr19.28v  2866  mob2  2906  euind  2913  reuind  2931  sbeqalb  3007  triun  4093  csbexga  4110  copsexg  4222  trssord  4358  trsuc  4400  trsucss  4401  abnexg  4424  ralxfrd  4440  rexxfrd  4441  ralxfrALT  4445  sucprcreg  4526  nlimsucg  4543  tfis  4560  relssres  4922  issref  4986  dmsnopg  5075  dfco2a  5104  imadif  5268  fvelima  5538  mptfvex  5571  fvmptdf  5573  fvmptf  5578  funfvima2  5717  funfvima3  5718  foco2  5722  isores3  5783  oprabid  5874  ovmpt4g  5964  ovmpos  5965  ov2gf  5966  ovmpodf  5973  suppssfv  6046  suppssov1  6047  fo2ndf  6195  rntpos  6225  tposf2  6236  nnmordi  6484  nnmord  6485  nnaordex  6495  ectocld  6567  qsel  6578  mapsn  6656  f1oeng  6723  mapen  6812  nneneq  6823  findcard2  6855  findcard2s  6856  ac6sfi  6864  fiintim  6894  sbthlem1  6922  pr2ne  7148  ltbtwnnqq  7356  prnmaddl  7431  genpcdl  7460  genpcuu  7461  ltaddpr  7538  lteupri  7558  recexprlemss1l  7576  recexprlemss1u  7577  cauappcvgprlemdisj  7592  lttrsr  7703  recexgt0sr  7714  mulgt0sr  7719  axprecex  7821  rereceu  7830  addlsub  8268  recexap  8550  0mnnnnn0  9146  prime  9290  zeo  9296  fnn0ind  9307  zindd  9309  btwnz  9310  lbzbi  9554  addmodlteq  10333  facwordi  10653  seq3coll  10755  qdenre  11144  climcau  11288  serf0  11293  zsumdc  11325  fsum2dlemstep  11375  fsum2d  11376  fsumabs  11406  fsumiun  11418  zproddc  11520  fprod2dlemstep  11563  fprod2d  11564  odd2np1  11810  ndvdssub  11867  dfgcd2  11947  nprm  12055  rpexp  12085  pc2dvds  12261  pcfac  12280  lmss  12886  lmtopcnp  12890  txcn  12915  txlm  12919  xmettri2  13001  blin2  13072  metcnp3  13151  limcresi  13275  logbgcd1irr  13525  lgsdir2lem2  13570  lgsne0  13579  2sqlem6  13596  2sqlem10  13601  bj-stim  13627  bj-stan  13628  bj-stand  13629  bj-stal  13630  bj-sbimedh  13652  bj-vtoclgft  13656  elabgft1  13659  elabgf2  13661