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  100  biimtrid  152  biimtrrid  153  imbitrid  154  adantld  278  adantrd  279  impel  280  mpan9  281  nsyli  649  pm2.36  804  pm4.72  827  pm2.18dc  855  con1dc  856  jadc  863  pm2.521dcALT  870  con1biimdc  873  condandc  881  pm5.18dc  883  pm2.68dc  894  annimdc  937  syl3an2  1272  syl2an23an  1299  xor3dc  1387  alrimdh  1479  spsd  1538  a5i  1543  19.21h  1557  hbnt  1653  hbae  1718  sbiedh  1787  exdistrfor  1800  sbcof2  1810  ax11a2  1821  ax11v  1827  sb4  1832  hbsb4t  2013  exmoeudc  2089  euimmo  2093  mopick  2104  r19.37  2629  spcimgft  2815  spcimegft  2817  rr19.28v  2879  mob2  2919  euind  2926  reuind  2944  sbeqalb  3021  triun  4116  csbexga  4133  copsexg  4246  trssord  4382  trsuc  4424  trsucss  4425  abnexg  4448  ralxfrd  4464  rexxfrd  4465  ralxfrALT  4469  sucprcreg  4550  nlimsucg  4567  tfis  4584  relssres  4947  issref  5013  dmsnopg  5102  dfco2a  5131  imadif  5298  fvelima  5569  mptfvex  5603  fvmptdf  5605  fvmptf  5610  funfvima2  5751  funfvima3  5752  foco2  5756  isores3  5818  oprabid  5909  ovmpt4g  5999  ovmpos  6000  ov2gf  6001  ovmpodf  6008  suppssfv  6081  suppssov1  6082  fo2ndf  6230  rntpos  6260  tposf2  6271  nnmordi  6519  nnmord  6520  nnaordex  6531  ectocld  6603  qsel  6614  mapsn  6692  f1oeng  6759  mapen  6848  nneneq  6859  findcard2  6891  findcard2s  6892  ac6sfi  6900  fiintim  6930  sbthlem1  6958  pr2ne  7193  ltbtwnnqq  7416  prnmaddl  7491  genpcdl  7520  genpcuu  7521  ltaddpr  7598  lteupri  7618  recexprlemss1l  7636  recexprlemss1u  7637  cauappcvgprlemdisj  7652  lttrsr  7763  recexgt0sr  7774  mulgt0sr  7779  axprecex  7881  rereceu  7890  addlsub  8329  recexap  8612  0mnnnnn0  9210  prime  9354  zeo  9360  fnn0ind  9371  zindd  9373  btwnz  9374  lbzbi  9618  addmodlteq  10400  facwordi  10722  seq3coll  10824  qdenre  11213  climcau  11357  serf0  11362  zsumdc  11394  fsum2dlemstep  11444  fsum2d  11445  fsumabs  11475  fsumiun  11487  zproddc  11589  fprod2dlemstep  11632  fprod2d  11633  odd2np1  11880  ndvdssub  11937  dfgcd2  12017  nprm  12125  rpexp  12155  pc2dvds  12331  pcfac  12350  mulgaddcom  13012  mulginvcom  13013  ringinvnz1ne0  13231  lmss  13785  lmtopcnp  13789  txcn  13814  txlm  13818  xmettri2  13900  blin2  13971  metcnp3  14050  limcresi  14174  logbgcd1irr  14424  lgsdir2lem2  14469  lgsne0  14478  2sqlem6  14506  2sqlem10  14511  bj-stim  14537  bj-stan  14538  bj-stand  14539  bj-stal  14540  bj-sbimedh  14562  bj-vtoclgft  14566  elabgft1  14569  elabgf2  14571