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  652  pm2.36  809  pm4.72  832  pm2.18dc  860  con1dc  861  jadc  868  pm2.521dcALT  875  con1biimdc  878  condandc  886  pm5.18dc  888  pm2.68dc  899  syl3an2  1305  syl2an23an  1333  xor3dc  1429  alrimdh  1525  spsd  1584  a5i  1589  19.21h  1603  hbnt  1699  hbae  1764  sbiedh  1833  exdistrfor  1846  sbcof2  1856  ax11a2  1867  ax11v  1873  sb4  1878  hbsb4t  2064  exmoeudc  2141  euimmo  2145  mopick  2156  r19.37  2683  spcimgft  2879  spcimegft  2881  rr19.28v  2943  mob2  2983  euind  2990  reuind  3008  sbeqalb  3085  triun  4195  csbexga  4212  copsexg  4330  trssord  4471  trsuc  4513  trsucss  4514  abnexg  4537  ralxfrd  4553  rexxfrd  4554  ralxfrALT  4558  sucprcreg  4641  nlimsucg  4658  tfis  4675  relssres  5043  issref  5111  dmsnopg  5200  dfco2a  5229  imadif  5401  fvelima  5687  mptfvex  5722  fvmptdf  5724  fvmptf  5729  funfvima2  5876  funfvima3  5877  foco2  5883  isores3  5945  oprabid  6039  ovmpt4g  6133  ovmpos  6134  ov2gf  6135  ovmpodf  6142  suppssfv  6220  suppssov1  6221  fo2ndf  6379  rntpos  6409  tposf2  6420  nnmordi  6670  nnmord  6671  nnaordex  6682  ectocld  6756  qsel  6767  mapsn  6845  f1oeng  6916  mapen  7015  nneneq  7026  findcard2  7059  findcard2s  7060  ac6sfi  7068  fiintim  7104  sbthlem1  7135  pr2ne  7376  ltbtwnnqq  7613  prnmaddl  7688  genpcdl  7717  genpcuu  7718  ltaddpr  7795  lteupri  7815  recexprlemss1l  7833  recexprlemss1u  7834  cauappcvgprlemdisj  7849  lttrsr  7960  recexgt0sr  7971  mulgt0sr  7976  axprecex  8078  rereceu  8087  addlsub  8527  recexap  8811  0mnnnnn0  9412  prime  9557  zeo  9563  fnn0ind  9574  zindd  9576  btwnz  9577  lbzbi  9823  addmodlteq  10632  facwordi  10974  seq3coll  11077  ccatalpha  11161  pfxccatin12lem2a  11274  qdenre  11728  climcau  11873  serf0  11878  zsumdc  11910  fsum2dlemstep  11960  fsum2d  11961  fsumabs  11991  fsumiun  12003  zproddc  12105  fprod2dlemstep  12148  fprod2d  12149  odd2np1  12399  ndvdssub  12456  bitsinv1lem  12487  dfgcd2  12550  nprm  12660  rpexp  12690  pc2dvds  12868  pcfac  12888  4sqlem12  12940  4sqlem17  12945  divsfval  13376  mulgaddcom  13698  mulginvcom  13699  ringinvnz1ne0  14027  lmss  14935  lmtopcnp  14939  txcn  14964  txlm  14968  xmettri2  15050  blin2  15121  metcnp3  15200  limcresi  15355  dvmptfsum  15414  logbgcd1irr  15656  lgsdir2lem2  15723  lgsne0  15732  2lgsoddprm  15807  2sqlem6  15814  2sqlem10  15819  uhgr0vb  15899  wlk1walkdom  16100  wlkv0  16110  wlklenvclwlk  16114  bj-stim  16165  bj-stan  16166  bj-stand  16167  bj-stal  16168  bj-sbimedh  16190  bj-vtoclgft  16194  elabgft1  16197  elabgf2  16199