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  1251  syl2an23an  1278  xor3dc  1366  alrimdh  1456  spsd  1519  a5i  1523  19.21h  1537  hbnt  1632  hbae  1697  sbiedh  1761  exdistrfor  1773  sbcof2  1783  ax11a2  1794  ax11v  1800  sb4  1805  hbsb4t  1989  exmoeudc  2063  euimmo  2067  mopick  2078  r19.37  2586  spcimgft  2765  spcimegft  2767  rr19.28v  2828  mob2  2868  euind  2875  reuind  2893  sbeqalb  2969  triun  4047  csbexga  4064  copsexg  4174  trssord  4310  trsuc  4352  trsucss  4353  abnexg  4375  ralxfrd  4391  rexxfrd  4392  ralxfrALT  4396  sucprcreg  4472  nlimsucg  4489  tfis  4505  relssres  4865  issref  4929  dmsnopg  5018  dfco2a  5047  imadif  5211  fvelima  5481  mptfvex  5514  fvmptdf  5516  fvmptf  5521  funfvima2  5658  funfvima3  5659  foco2  5663  isores3  5724  oprabid  5811  ovmpt4g  5901  ovmpos  5902  ov2gf  5903  ovmpodf  5910  suppssfv  5986  suppssov1  5987  fo2ndf  6132  rntpos  6162  tposf2  6173  nnmordi  6420  nnmord  6421  nnaordex  6431  ectocld  6503  qsel  6514  mapsn  6592  f1oeng  6659  mapen  6748  nneneq  6759  findcard2  6791  findcard2s  6792  ac6sfi  6800  fiintim  6825  sbthlem1  6853  pr2ne  7065  ltbtwnnqq  7247  prnmaddl  7322  genpcdl  7351  genpcuu  7352  ltaddpr  7429  lteupri  7449  recexprlemss1l  7467  recexprlemss1u  7468  cauappcvgprlemdisj  7483  lttrsr  7594  recexgt0sr  7605  mulgt0sr  7610  axprecex  7712  rereceu  7721  addlsub  8156  recexap  8438  0mnnnnn0  9033  prime  9174  zeo  9180  fnn0ind  9191  zindd  9193  btwnz  9194  lbzbi  9435  addmodlteq  10202  facwordi  10518  seq3coll  10617  qdenre  11006  climcau  11148  serf0  11153  zsumdc  11185  fsum2dlemstep  11235  fsum2d  11236  fsumabs  11266  fsumiun  11278  zproddc  11380  odd2np1  11606  ndvdssub  11663  dfgcd2  11738  nprm  11840  rpexp  11867  lmss  12454  lmtopcnp  12458  txcn  12483  txlm  12487  xmettri2  12569  blin2  12640  metcnp3  12719  limcresi  12843  logbgcd1irr  13092  bj-stim  13125  bj-stan  13126  bj-stand  13127  bj-stal  13128  bj-sbimedh  13149  bj-vtoclgft  13153  elabgft1  13156  elabgf2  13158