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  650  pm2.36  805  pm4.72  828  pm2.18dc  856  con1dc  857  jadc  864  pm2.521dcALT  871  con1biimdc  874  condandc  882  pm5.18dc  884  pm2.68dc  895  syl3an2  1283  syl2an23an  1311  xor3dc  1406  alrimdh  1501  spsd  1560  a5i  1565  19.21h  1579  hbnt  1675  hbae  1740  sbiedh  1809  exdistrfor  1822  sbcof2  1832  ax11a2  1843  ax11v  1849  sb4  1854  hbsb4t  2040  exmoeudc  2116  euimmo  2120  mopick  2131  r19.37  2657  spcimgft  2848  spcimegft  2850  rr19.28v  2912  mob2  2952  euind  2959  reuind  2977  sbeqalb  3054  triun  4154  csbexga  4171  copsexg  4287  trssord  4426  trsuc  4468  trsucss  4469  abnexg  4492  ralxfrd  4508  rexxfrd  4509  ralxfrALT  4513  sucprcreg  4596  nlimsucg  4613  tfis  4630  relssres  4996  issref  5064  dmsnopg  5153  dfco2a  5182  imadif  5353  fvelima  5629  mptfvex  5664  fvmptdf  5666  fvmptf  5671  funfvima2  5816  funfvima3  5817  foco2  5821  isores3  5883  oprabid  5975  ovmpt4g  6067  ovmpos  6068  ov2gf  6069  ovmpodf  6076  suppssfv  6153  suppssov1  6154  fo2ndf  6312  rntpos  6342  tposf2  6353  nnmordi  6601  nnmord  6602  nnaordex  6613  ectocld  6687  qsel  6698  mapsn  6776  f1oeng  6847  mapen  6942  nneneq  6953  findcard2  6985  findcard2s  6986  ac6sfi  6994  fiintim  7027  sbthlem1  7058  pr2ne  7299  ltbtwnnqq  7527  prnmaddl  7602  genpcdl  7631  genpcuu  7632  ltaddpr  7709  lteupri  7729  recexprlemss1l  7747  recexprlemss1u  7748  cauappcvgprlemdisj  7763  lttrsr  7874  recexgt0sr  7885  mulgt0sr  7890  axprecex  7992  rereceu  8001  addlsub  8441  recexap  8725  0mnnnnn0  9326  prime  9471  zeo  9477  fnn0ind  9488  zindd  9490  btwnz  9491  lbzbi  9736  addmodlteq  10541  facwordi  10883  seq3coll  10985  qdenre  11484  climcau  11629  serf0  11634  zsumdc  11666  fsum2dlemstep  11716  fsum2d  11717  fsumabs  11747  fsumiun  11759  zproddc  11861  fprod2dlemstep  11904  fprod2d  11905  odd2np1  12155  ndvdssub  12212  bitsinv1lem  12243  dfgcd2  12306  nprm  12416  rpexp  12446  pc2dvds  12624  pcfac  12644  4sqlem12  12696  4sqlem17  12701  divsfval  13131  mulgaddcom  13453  mulginvcom  13454  ringinvnz1ne0  13782  lmss  14689  lmtopcnp  14693  txcn  14718  txlm  14722  xmettri2  14804  blin2  14875  metcnp3  14954  limcresi  15109  dvmptfsum  15168  logbgcd1irr  15410  lgsdir2lem2  15477  lgsne0  15486  2lgsoddprm  15561  2sqlem6  15568  2sqlem10  15573  bj-stim  15644  bj-stan  15645  bj-stand  15646  bj-stal  15647  bj-sbimedh  15669  bj-vtoclgft  15673  elabgft1  15676  elabgf2  15678