Theorem sylc 62

Description: A syllogism inference combined with contraction. (Contributed by NM, 4-May-1994.) (Revised by NM, 13-Jul-2013.)

Hypotheses

Ref	Expression
sylc.1	|- ( ph -> ps )
sylc.2	|- ( ph -> ch )
sylc.3	|- ( ps -> ( ch -> th ) )

Assertion

Ref	Expression
sylc	|- ( ph -> th )

Proof of Theorem sylc

Step	Hyp	Ref	Expression
1		sylc.1	. . 3 |- ( ph -> ps )
2		sylc.2	. . 3 |- ( ph -> ch )
3		sylc.3	. . 3 |- ( ps -> ( ch -> th ) )
4	1, 2, 3	syl2im 38	. 2 |- ( ph -> ( ph -> th ) )
5	4	pm2.43i 49	1 |- ( 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:  syl3c  63  mpsyl  65  imp  124  2thd  175  jca  306  syl2anc  411  jc  652  jcnd  654  annimdc  940  pm4.55dc  941  orandc  942  dn1dc  963  syl2an23an  1312  xordidc  1419  nfimd  1608  exlimd2  1618  elex22  2787  elex2  2788  spcimdv  2857  spcimedv  2859  spcedv  2862  rspcdva  2882  elabd  2918  spsbcd  3011  opth  4282  euotd  4300  ssorduni  4536  tfisi  4636  omsinds  4671  nnpredcl  4672  sotri2  5081  sotri3  5082  unielrel  5211  funmo  5287  fnfvima  5821  fliftfun  5867  fliftval  5871  riota5f  5926  riotass2  5928  fovcld  6052  oprssdmm  6259  tfrlem5  6402  tfrlemibxssdm  6415  tfrlemibfn  6416  tfrlemiex  6419  tfr1onlemsucfn  6428  tfr1onlemsucaccv  6429  tfr1onlembxssdm  6431  tfr1onlembfn  6432  tfr1onlemex  6435  tfr1onlemres  6437  tfrcllemsucfn  6441  tfrcllemsucaccv  6442  tfrcllembxssdm  6444  tfrcllembfn  6445  tfrcllemex  6448  tfrcllemres  6450  tfrcl  6452  rdgisucinc  6473  frecabex  6486  frecabcl  6487  nntr2  6591  ertr  6637  qliftlem  6702  th3q  6729  resixp  6822  f1dom2g  6849  dom3d  6867  domssr  6871  en1  6893  xpdom3m  6931  xpf1o  6943  phplem4dom  6961  phpm  6964  phpelm  6965  findcard  6987  finexdc  7001  fiintim  7030  fisseneq  7033  ssfirab  7035  opabfi  7037  f1dmvrnfibi  7048  iunfidisj  7050  fidcenumlemrk  7058  dcfi  7085  suplub2ti  7105  supelti  7106  ordiso2  7139  caseinl  7195  caseinr  7196  djudom  7197  difinfsn  7204  difinfinf  7205  ctm  7213  enumct  7219  nnnninfeq  7232  ismkvnex  7259  exmidfodomrlemr  7312  exmidfodomrlemrALT  7313  acfun  7321  exmidontriimlem2  7336  exmidontriimlem3  7337  exmidapne  7374  cc2lem  7380  cc3  7382  recexnq  7505  ltbtwnnqq  7530  addnnnq0  7564  mulnnnq0  7565  prarloclemn  7614  prarloc  7618  distrlem1prl  7697  distrlem1pru  7698  distrlem4prl  7699  distrlem4pru  7700  ltexprlemrl  7725  cauappcvgprlemladdru  7771  cauappcvgprlemladdrl  7772  addsrpr  7860  mulsrpr  7861  map2psrprg  7920  axpre-suploclemres  8016  lemul12a  8937  lemulge11  8941  sup3exmid  9032  nngt0  9063  nn0ge0  9322  nn0ge2m1nn  9357  zletric  9418  zlelttric  9419  nn0n0n1ge2b  9454  nn0ind-raph  9492  supinfneg  9718  infsupneg  9719  infregelbex  9721  rpge0  9790  fz0fzelfz0  10251  fz0fzdiffz0  10254  ige2m2fzo  10329  elfzodifsumelfzo  10332  elfzom1elp1fzo  10333  exfzdc  10371  zsupcllemstep  10374  infssuzex  10378  qletric  10386  qlelttric  10387  rebtwn2zlemshrink  10398  frecuzrdgtcl  10559  frecuzrdg0  10560  frecuzrdgfunlem  10566  frecuzrdg0t  10569  frecuzrdgsuctlem  10570  frecfzennn  10573  seq3f1olemstep  10661  expcl2lemap  10698  leexp1a  10741  expnbnd  10810  faclbnd  10888  faclbnd6  10891  facavg  10893  fihasheqf1oi  10934  fihashf1rn  10935  fihashss  10963  fiubm  10975  seq3coll  10989  wrdsymb0  11028  wrdlenge2n0  11031  ccatsymb  11061  pfxnd  11143  pfxccat1  11156  resqrexlemdecn  11356  qabsor  11419  cau3lem  11458  xrmaxiflemab  11591  xrmaxadd  11605  climcn2  11653  sumeq2  11703  sumrbdclem  11721  summodclem3  11724  summodclem2a  11725  zsumdc  11728  fsumgcl  11730  fsum3  11731  isumss  11735  fsumadd  11750  fsum2dlemstep  11778  fisum0diag2  11791  fsummulc2  11792  modfsummodlemstep  11801  fsumabs  11809  fsumrelem  11815  fsumiun  11821  isumshft  11834  mertenslem2  11880  prodeq2  11901  prodrbdclem  11915  prodmodclem3  11919  prodmodclem2a  11920  zproddc  11923  fprodseq  11927  fprodmul  11935  fprodconst  11964  fprodap0  11965  fprod2dlemstep  11966  fprodrec  11973  fprodsplit1f  11978  fprodap0f  11980  fprodle  11984  sin02gt0  12108  efieq1re  12116  p1modz1  12138  dvdsleabs2  12190  4dvdseven  12261  bitsfzo  12299  bitsinv1lem  12305  gcdeq0  12331  rppwr  12382  uzwodc  12391  algfx  12407  eucalgcvga  12413  lcmmndc  12417  lcmeq0  12426  qredeq  12451  isprm3  12473  rpexp  12508  sqpweven  12530  2sqpwodd  12531  phicl2  12569  phibnd  12572  phiprmpw  12577  fermltl  12589  pythagtriplem4  12624  pythagtriplem6  12626  pythagtriplem7  12627  pythagtriplem12  12631  pythagtriplem13  12632  pythagtriplem14  12633  pythagtriplem16  12635  pcdvdsb  12676  pc2dvds  12686  difsqpwdvds  12694  pcmpt  12699  pcmptdvds  12701  fldivp1  12704  prmpwdvds  12711  infpnlem1  12715  1arith  12723  4sqlem11  12757  ennnfonelemk  12804  ennnfonelemhom  12819  ennnfonelemrnh  12820  ennnfonelemf1  12822  ctinf  12834  ctiunctlemudc  12841  ctiunctlemf  12842  nninfdclemp1  12854  strslfvd  12907  strslfv2d  12908  strslssd  12912  imasival  13171  imasbas  13172  imasplusg  13173  imasaddfnlemg  13179  imasaddvallemg  13180  qusaddvallemg  13198  qusaddflemg  13199  qusaddval  13200  qusaddf  13201  qusmulval  13202  qusmulf  13203  lidrididd  13247  gsumfzval  13256  sgrpidmndm  13285  gsumfzz  13360  qusgrp2  13482  mulgnegnn  13501  eqgen  13596  rinvmod  13678  gsumfzconst  13710  qusrng  13753  srgdilem  13764  ringdilem  13807  qusring2  13861  lssintclm  14179  gsumfzfsumlemm  14382  mplsubgfilemm  14493  eltg3  14562  iuncld  14620  cnss2  14732  txcnp  14776  uptx  14779  xblm  14922  metss  14999  fsumcncntop  15072  rescncf  15086  dedekindeulemlu  15126  suplociccex  15130  dedekindicclemlu  15135  dedekindicc  15138  ivthdec  15149  limccnp2lem  15181  dvaddxx  15208  dvmulxx  15209  dvrecap  15218  reeff1olem  15276  perfectlem2  15505  lgsval  15514  lgsfvalg  15515  lgsfcl2  15516  lgscllem  15517  lgsval2lem  15520  lgsneg  15534  lgsdir2  15543  lgsdir  15545  lgsdi  15547  lgsne0  15548  lgsdirnn0  15557  lgsdinn0  15558  gausslemma2dlem0c  15561  m1lgs  15595  2lgslem1  15601  2lgs  15614  2lgsoddprm  15623  2sqlem6  15630  sumdc2  15772  pwle2  15972  subctctexmid  15974  nninfsellemeq  15988  nnnninfex  15996  exmidsbthrlem  15998  cndcap  16035