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  656  jcnd  658  annimdc  946  pm4.55dc  947  orandc  948  dn1dc  969  syl2an23an  1336  xordidc  1444  nfimd  1634  exlimd2  1644  elex22  2819  elex2  2820  spcimdv  2891  spcimedv  2893  spcedv  2896  rspcdva  2916  elabd  2952  spsbcd  3045  opth  4335  euotd  4353  ssorduni  4591  tfisi  4691  omsinds  4726  nnpredcl  4727  sotri2  5141  sotri3  5142  unielrel  5271  funmo  5348  fnfvima  5899  resfvresima  5901  fliftfun  5947  fliftval  5951  riota5f  6008  riotass2  6010  fovcld  6136  oprssdmm  6343  funsssuppss  6436  tfrlem5  6523  tfrlemibxssdm  6536  tfrlemibfn  6537  tfrlemiex  6540  tfr1onlemsucfn  6549  tfr1onlemsucaccv  6550  tfr1onlembxssdm  6552  tfr1onlembfn  6553  tfr1onlemex  6556  tfr1onlemres  6558  tfrcllemsucfn  6562  tfrcllemsucaccv  6563  tfrcllembxssdm  6565  tfrcllembfn  6566  tfrcllemex  6569  tfrcllemres  6571  tfrcl  6573  rdgisucinc  6594  frecabex  6607  frecabcl  6608  nntr2  6714  ertr  6760  qliftlem  6825  th3q  6852  resixp  6945  f1dom2g  6972  dom3d  6990  domssr  6994  en1  7016  xpdom3m  7061  xpf1o  7073  phplem4dom  7091  phpm  7095  phpelm  7096  findcard  7120  finexdc  7135  fiintim  7166  fisseneq  7170  ssfirab  7172  opabfi  7175  f1dmvrnfibi  7186  iunfidisj  7188  fidcenumlemrk  7196  dcfi  7240  suplub2ti  7260  supelti  7261  ordiso2  7294  caseinl  7350  caseinr  7351  djudom  7352  difinfsn  7359  difinfinf  7360  ctm  7368  enumct  7374  nnnninfeq  7387  ismkvnex  7414  exmidfodomrlemr  7473  exmidfodomrlemrALT  7474  acfun  7482  exmidontriimlem2  7497  exmidontriimlem3  7498  exmidapne  7539  cc2lem  7545  cc3  7547  recexnq  7670  ltbtwnnqq  7695  addnnnq0  7729  mulnnnq0  7730  prarloclemn  7779  prarloc  7783  distrlem1prl  7862  distrlem1pru  7863  distrlem4prl  7864  distrlem4pru  7865  ltexprlemrl  7890  cauappcvgprlemladdru  7936  cauappcvgprlemladdrl  7937  addsrpr  8025  mulsrpr  8026  map2psrprg  8085  axpre-suploclemres  8181  lemul12a  9101  lemulge11  9105  sup3exmid  9196  nngt0  9227  nn0ge0  9486  nn0ge2m1nn  9523  zletric  9584  zlelttric  9585  nn0n0n1ge2b  9620  nn0ind-raph  9658  supinfneg  9890  infsupneg  9891  infregelbex  9893  rpge0  9962  fz0fzelfz0  10424  fz0fzdiffz0  10427  ige2m2fzo  10506  elfzodifsumelfzo  10509  elfzom1elp1fzo  10510  exfzdc  10549  zsupcllemstep  10552  infssuzex  10556  qletric  10564  qlelttric  10565  rebtwn2zlemshrink  10576  frecuzrdgtcl  10737  frecuzrdg0  10738  frecuzrdgfunlem  10744  frecuzrdg0t  10747  frecuzrdgsuctlem  10748  frecfzennn  10751  seq3f1olemstep  10839  expcl2lemap  10876  leexp1a  10919  expnbnd  10988  faclbnd  11066  faclbnd6  11069  facavg  11071  fihasheqf1oi  11112  fihashf1rn  11113  fihashss  11143  fiubm  11155  seq3coll  11169  wrdsymb0  11212  wrdlenge2n0  11215  ccatsymb  11245  pfxnd  11336  pfxccat1  11349  swrdpfx  11354  pfxpfx  11355  wrd2ind  11370  pfxccatin12  11380  pfxccat3  11381  swrdccat  11382  pfxccatpfx1  11383  pfxccatpfx2  11384  swrdccatin1d  11390  pfxccatin12d  11392  resqrexlemdecn  11652  qabsor  11715  cau3lem  11754  xrmaxiflemab  11887  xrmaxadd  11901  climcn2  11949  sumeq2  11999  sumrbdclem  12018  summodclem3  12021  summodclem2a  12022  zsumdc  12025  fsumgcl  12027  fsum3  12028  isumss  12032  fsumadd  12047  fsum2dlemstep  12075  fisum0diag2  12088  fsummulc2  12089  modfsummodlemstep  12098  fsumabs  12106  fsumrelem  12112  fsumiun  12118  isumshft  12131  mertenslem2  12177  prodeq2  12198  prodrbdclem  12212  prodmodclem3  12216  prodmodclem2a  12217  zproddc  12220  fprodseq  12224  fprodmul  12232  fprodconst  12261  fprodap0  12262  fprod2dlemstep  12263  fprodrec  12270  fprodsplit1f  12275  fprodap0f  12277  fprodle  12281  sin02gt0  12405  efieq1re  12413  p1modz1  12435  dvdsleabs2  12487  4dvdseven  12558  bitsfzo  12596  bitsinv1lem  12602  gcdeq0  12628  rppwr  12679  uzwodc  12688  algfx  12704  eucalgcvga  12710  lcmmndc  12714  lcmeq0  12723  qredeq  12748  isprm3  12770  rpexp  12805  sqpweven  12827  2sqpwodd  12828  phicl2  12866  phibnd  12869  phiprmpw  12874  fermltl  12886  pythagtriplem4  12921  pythagtriplem6  12923  pythagtriplem7  12924  pythagtriplem12  12928  pythagtriplem13  12929  pythagtriplem14  12930  pythagtriplem16  12932  pcdvdsb  12973  pc2dvds  12983  difsqpwdvds  12991  pcmpt  12996  pcmptdvds  12998  fldivp1  13001  prmpwdvds  13008  infpnlem1  13012  1arith  13020  4sqlem11  13054  ennnfonelemk  13101  ennnfonelemhom  13116  ennnfonelemrnh  13117  ennnfonelemf1  13119  ctinf  13131  ctiunctlemudc  13138  ctiunctlemf  13139  nninfdclemp1  13151  strslfvd  13204  strslfv2d  13205  strslssd  13209  imasival  13469  imasbas  13470  imasplusg  13471  imasaddfnlemg  13477  imasaddvallemg  13478  qusaddvallemg  13496  qusaddflemg  13497  qusaddval  13498  qusaddf  13499  qusmulval  13500  qusmulf  13501  lidrididd  13545  gsumfzval  13554  sgrpidmndm  13583  gsumfzz  13658  qusgrp2  13780  mulgnegnn  13799  eqgen  13894  rinvmod  13976  gsumfzconst  14008  qusrng  14052  srgdilem  14063  ringdilem  14106  qusring2  14160  lssintclm  14480  gsumfzfsumlemm  14683  mplsubgfilemm  14799  eltg3  14868  iuncld  14926  cnss2  15038  txcnp  15082  uptx  15085  xblm  15228  metss  15305  fsumcncntop  15378  rescncf  15392  dedekindeulemlu  15432  suplociccex  15436  dedekindicclemlu  15441  dedekindicc  15444  ivthdec  15455  limccnp2lem  15487  dvaddxx  15514  dvmulxx  15515  dvrecap  15524  reeff1olem  15582  perfectlem2  15814  lgsval  15823  lgsfvalg  15824  lgsfcl2  15825  lgscllem  15826  lgsval2lem  15829  lgsneg  15843  lgsdir2  15852  lgsdir  15854  lgsdi  15856  lgsne0  15857  lgsdirnn0  15866  lgsdinn0  15867  gausslemma2dlem0c  15870  m1lgs  15904  2lgslem1  15910  2lgs  15923  2lgsoddprm  15932  2sqlem6  15939  incistruhgr  16031  upgredg  16085  uhgr2edg  16147  usgriedgdomord  16166  wlkpropg  16265  wlkvtxeledgg  16285  wlk2f  16292  clwwlknonccat  16374  clwwlknonex2lem2  16379  eupth2lem3lem4fi  16414  eupth2lem3lem7fi  16415  sumdc2  16517  pwle2  16720  subctctexmid  16722  nninfsellemeq  16740  nnnninfex  16748  exmidsbthrlem  16750  cndcap  16792  gfsump1  16815