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  813  const  838  pm2.18dc  841  con1dc  842  jadc  849  pm2.521dcALT  856  con1biimdc  859  condandc  867  pm5.18dc  869  pm2.68dc  880  annimdc  922  syl3an2  1254  syl2an23an  1281  xor3dc  1369  alrimdh  1459  spsd  1518  a5i  1523  19.21h  1537  hbnt  1633  hbae  1698  sbiedh  1767  exdistrfor  1780  sbcof2  1790  ax11a2  1801  ax11v  1807  sb4  1812  hbsb4t  1993  exmoeudc  2069  euimmo  2073  mopick  2084  r19.37  2609  spcimgft  2788  spcimegft  2790  rr19.28v  2852  mob2  2892  euind  2899  reuind  2917  sbeqalb  2993  triun  4075  csbexga  4092  copsexg  4203  trssord  4339  trsuc  4381  trsucss  4382  abnexg  4404  ralxfrd  4420  rexxfrd  4421  ralxfrALT  4425  sucprcreg  4506  nlimsucg  4523  tfis  4540  relssres  4901  issref  4965  dmsnopg  5054  dfco2a  5083  imadif  5247  fvelima  5517  mptfvex  5550  fvmptdf  5552  fvmptf  5557  funfvima2  5694  funfvima3  5695  foco2  5699  isores3  5760  oprabid  5847  ovmpt4g  5937  ovmpos  5938  ov2gf  5939  ovmpodf  5946  suppssfv  6022  suppssov1  6023  fo2ndf  6168  rntpos  6198  tposf2  6209  nnmordi  6456  nnmord  6457  nnaordex  6467  ectocld  6539  qsel  6550  mapsn  6628  f1oeng  6695  mapen  6784  nneneq  6795  findcard2  6827  findcard2s  6828  ac6sfi  6836  fiintim  6866  sbthlem1  6894  pr2ne  7110  ltbtwnnqq  7318  prnmaddl  7393  genpcdl  7422  genpcuu  7423  ltaddpr  7500  lteupri  7520  recexprlemss1l  7538  recexprlemss1u  7539  cauappcvgprlemdisj  7554  lttrsr  7665  recexgt0sr  7676  mulgt0sr  7681  axprecex  7783  rereceu  7792  addlsub  8228  recexap  8510  0mnnnnn0  9105  prime  9246  zeo  9252  fnn0ind  9263  zindd  9265  btwnz  9266  lbzbi  9507  addmodlteq  10279  facwordi  10596  seq3coll  10695  qdenre  11084  climcau  11226  serf0  11231  zsumdc  11263  fsum2dlemstep  11313  fsum2d  11314  fsumabs  11344  fsumiun  11356  zproddc  11458  fprod2dlemstep  11501  fprod2d  11502  odd2np1  11745  ndvdssub  11802  dfgcd2  11878  nprm  11980  rpexp  12007  lmss  12606  lmtopcnp  12610  txcn  12635  txlm  12639  xmettri2  12721  blin2  12792  metcnp3  12871  limcresi  12995  logbgcd1irr  13244  bj-stim  13278  bj-stan  13279  bj-stand  13280  bj-stal  13281  bj-sbimedh  13304  bj-vtoclgft  13308  elabgft1  13311  elabgf2  13313