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  4194  csbexga  4211  copsexg  4329  trssord  4470  trsuc  4512  trsucss  4513  abnexg  4536  ralxfrd  4552  rexxfrd  4553  ralxfrALT  4557  sucprcreg  4640  nlimsucg  4657  tfis  4674  relssres  5042  issref  5110  dmsnopg  5199  dfco2a  5228  imadif  5400  fvelima  5684  mptfvex  5719  fvmptdf  5721  fvmptf  5726  funfvima2  5871  funfvima3  5872  foco2  5876  isores3  5938  oprabid  6032  ovmpt4g  6126  ovmpos  6127  ov2gf  6128  ovmpodf  6135  suppssfv  6212  suppssov1  6213  fo2ndf  6371  rntpos  6401  tposf2  6412  nnmordi  6660  nnmord  6661  nnaordex  6672  ectocld  6746  qsel  6757  mapsn  6835  f1oeng  6906  mapen  7003  nneneq  7014  findcard2  7047  findcard2s  7048  ac6sfi  7056  fiintim  7089  sbthlem1  7120  pr2ne  7361  ltbtwnnqq  7598  prnmaddl  7673  genpcdl  7702  genpcuu  7703  ltaddpr  7780  lteupri  7800  recexprlemss1l  7818  recexprlemss1u  7819  cauappcvgprlemdisj  7834  lttrsr  7945  recexgt0sr  7956  mulgt0sr  7961  axprecex  8063  rereceu  8072  addlsub  8512  recexap  8796  0mnnnnn0  9397  prime  9542  zeo  9548  fnn0ind  9559  zindd  9561  btwnz  9562  lbzbi  9807  addmodlteq  10615  facwordi  10957  seq3coll  11059  pfxccatin12lem2a  11254  qdenre  11708  climcau  11853  serf0  11858  zsumdc  11890  fsum2dlemstep  11940  fsum2d  11941  fsumabs  11971  fsumiun  11983  zproddc  12085  fprod2dlemstep  12128  fprod2d  12129  odd2np1  12379  ndvdssub  12436  bitsinv1lem  12467  dfgcd2  12530  nprm  12640  rpexp  12670  pc2dvds  12848  pcfac  12868  4sqlem12  12920  4sqlem17  12925  divsfval  13356  mulgaddcom  13678  mulginvcom  13679  ringinvnz1ne0  14007  lmss  14914  lmtopcnp  14918  txcn  14943  txlm  14947  xmettri2  15029  blin2  15100  metcnp3  15179  limcresi  15334  dvmptfsum  15393  logbgcd1irr  15635  lgsdir2lem2  15702  lgsne0  15711  2lgsoddprm  15786  2sqlem6  15793  2sqlem10  15798  uhgr0vb  15878  bj-stim  16068  bj-stan  16069  bj-stand  16070  bj-stal  16071  bj-sbimedh  16093  bj-vtoclgft  16097  elabgft1  16100  elabgf2  16102