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  2880  spcimegft  2882  rr19.28v  2944  mob2  2984  euind  2991  reuind  3009  sbeqalb  3086  triun  4198  csbexga  4215  copsexg  4334  trssord  4475  trsuc  4517  trsucss  4518  abnexg  4541  ralxfrd  4557  rexxfrd  4558  ralxfrALT  4562  sucprcreg  4645  nlimsucg  4662  tfis  4679  relssres  5049  issref  5117  dmsnopg  5206  dfco2a  5235  imadif  5407  fvelima  5693  mptfvex  5728  fvmptdf  5730  fvmptf  5735  funfvima2  5882  funfvima3  5883  foco2  5889  isores3  5951  oprabid  6045  ovmpt4g  6139  ovmpos  6140  ov2gf  6141  ovmpodf  6148  suppssfv  6226  suppssov1  6227  fo2ndf  6387  rntpos  6418  tposf2  6429  nnmordi  6679  nnmord  6680  nnaordex  6691  ectocld  6765  qsel  6776  mapsn  6854  f1oeng  6925  mapen  7027  nneneq  7038  findcard2  7071  findcard2s  7072  ac6sfi  7080  fiintim  7116  sbthlem1  7147  pr2ne  7388  ltbtwnnqq  7625  prnmaddl  7700  genpcdl  7729  genpcuu  7730  ltaddpr  7807  lteupri  7827  recexprlemss1l  7845  recexprlemss1u  7846  cauappcvgprlemdisj  7861  lttrsr  7972  recexgt0sr  7983  mulgt0sr  7988  axprecex  8090  rereceu  8099  addlsub  8539  recexap  8823  0mnnnnn0  9424  prime  9569  zeo  9575  fnn0ind  9586  zindd  9588  btwnz  9589  lbzbi  9840  addmodlteq  10650  facwordi  10992  seq3coll  11096  ccatalpha  11180  pfxccatin12lem2a  11298  qdenre  11753  climcau  11898  serf0  11903  zsumdc  11935  fsum2dlemstep  11985  fsum2d  11986  fsumabs  12016  fsumiun  12028  zproddc  12130  fprod2dlemstep  12173  fprod2d  12174  odd2np1  12424  ndvdssub  12481  bitsinv1lem  12512  dfgcd2  12575  nprm  12685  rpexp  12715  pc2dvds  12893  pcfac  12913  4sqlem12  12965  4sqlem17  12970  divsfval  13401  mulgaddcom  13723  mulginvcom  13724  ringinvnz1ne0  14052  lmss  14960  lmtopcnp  14964  txcn  14989  txlm  14993  xmettri2  15075  blin2  15146  metcnp3  15225  limcresi  15380  dvmptfsum  15439  logbgcd1irr  15681  lgsdir2lem2  15748  lgsne0  15757  2lgsoddprm  15832  2sqlem6  15839  2sqlem10  15844  uhgr0vb  15925  wlk1walkdom  16156  wlkv0  16166  wlklenvclwlk  16170  bj-stim  16278  bj-stan  16279  bj-stand  16280  bj-stal  16281  bj-sbimedh  16303  bj-vtoclgft  16307  elabgft1  16310  elabgf2  16312