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  945  pm4.55dc  946  orandc  947  dn1dc  968  syl2an23an  1335  xordidc  1443  nfimd  1633  exlimd2  1643  elex22  2818  elex2  2819  spcimdv  2890  spcimedv  2892  spcedv  2895  rspcdva  2915  elabd  2951  spsbcd  3044  opth  4329  euotd  4347  ssorduni  4585  tfisi  4685  omsinds  4720  nnpredcl  4721  sotri2  5134  sotri3  5135  unielrel  5264  funmo  5341  fnfvima  5889  resfvresima  5891  fliftfun  5937  fliftval  5941  riota5f  5998  riotass2  6000  fovcld  6126  oprssdmm  6334  tfrlem5  6480  tfrlemibxssdm  6493  tfrlemibfn  6494  tfrlemiex  6497  tfr1onlemsucfn  6506  tfr1onlemsucaccv  6507  tfr1onlembxssdm  6509  tfr1onlembfn  6510  tfr1onlemex  6513  tfr1onlemres  6515  tfrcllemsucfn  6519  tfrcllemsucaccv  6520  tfrcllembxssdm  6522  tfrcllembfn  6523  tfrcllemex  6526  tfrcllemres  6528  tfrcl  6530  rdgisucinc  6551  frecabex  6564  frecabcl  6565  nntr2  6671  ertr  6717  qliftlem  6782  th3q  6809  resixp  6902  f1dom2g  6929  dom3d  6947  domssr  6951  en1  6973  xpdom3m  7018  xpf1o  7030  phplem4dom  7048  phpm  7052  phpelm  7053  findcard  7077  finexdc  7092  fiintim  7123  fisseneq  7127  ssfirab  7129  opabfi  7132  f1dmvrnfibi  7143  iunfidisj  7145  fidcenumlemrk  7153  dcfi  7180  suplub2ti  7200  supelti  7201  ordiso2  7234  caseinl  7290  caseinr  7291  djudom  7292  difinfsn  7299  difinfinf  7300  ctm  7308  enumct  7314  nnnninfeq  7327  ismkvnex  7354  exmidfodomrlemr  7413  exmidfodomrlemrALT  7414  acfun  7422  exmidontriimlem2  7437  exmidontriimlem3  7438  exmidapne  7479  cc2lem  7485  cc3  7487  recexnq  7610  ltbtwnnqq  7635  addnnnq0  7669  mulnnnq0  7670  prarloclemn  7719  prarloc  7723  distrlem1prl  7802  distrlem1pru  7803  distrlem4prl  7804  distrlem4pru  7805  ltexprlemrl  7830  cauappcvgprlemladdru  7876  cauappcvgprlemladdrl  7877  addsrpr  7965  mulsrpr  7966  map2psrprg  8025  axpre-suploclemres  8121  lemul12a  9042  lemulge11  9046  sup3exmid  9137  nngt0  9168  nn0ge0  9427  nn0ge2m1nn  9462  zletric  9523  zlelttric  9524  nn0n0n1ge2b  9559  nn0ind-raph  9597  supinfneg  9829  infsupneg  9830  infregelbex  9832  rpge0  9901  fz0fzelfz0  10362  fz0fzdiffz0  10365  ige2m2fzo  10443  elfzodifsumelfzo  10446  elfzom1elp1fzo  10447  exfzdc  10486  zsupcllemstep  10489  infssuzex  10493  qletric  10501  qlelttric  10502  rebtwn2zlemshrink  10513  frecuzrdgtcl  10674  frecuzrdg0  10675  frecuzrdgfunlem  10681  frecuzrdg0t  10684  frecuzrdgsuctlem  10685  frecfzennn  10688  seq3f1olemstep  10776  expcl2lemap  10813  leexp1a  10856  expnbnd  10925  faclbnd  11003  faclbnd6  11006  facavg  11008  fihasheqf1oi  11049  fihashf1rn  11050  fihashss  11080  fiubm  11092  seq3coll  11106  wrdsymb0  11146  wrdlenge2n0  11149  ccatsymb  11179  pfxnd  11270  pfxccat1  11283  swrdpfx  11288  pfxpfx  11289  wrd2ind  11304  pfxccatin12  11314  pfxccat3  11315  swrdccat  11316  pfxccatpfx1  11317  pfxccatpfx2  11318  swrdccatin1d  11324  pfxccatin12d  11326  resqrexlemdecn  11573  qabsor  11636  cau3lem  11675  xrmaxiflemab  11808  xrmaxadd  11822  climcn2  11870  sumeq2  11920  sumrbdclem  11939  summodclem3  11942  summodclem2a  11943  zsumdc  11946  fsumgcl  11948  fsum3  11949  isumss  11953  fsumadd  11968  fsum2dlemstep  11996  fisum0diag2  12009  fsummulc2  12010  modfsummodlemstep  12019  fsumabs  12027  fsumrelem  12033  fsumiun  12039  isumshft  12052  mertenslem2  12098  prodeq2  12119  prodrbdclem  12133  prodmodclem3  12137  prodmodclem2a  12138  zproddc  12141  fprodseq  12145  fprodmul  12153  fprodconst  12182  fprodap0  12183  fprod2dlemstep  12184  fprodrec  12191  fprodsplit1f  12196  fprodap0f  12198  fprodle  12202  sin02gt0  12326  efieq1re  12334  p1modz1  12356  dvdsleabs2  12408  4dvdseven  12479  bitsfzo  12517  bitsinv1lem  12523  gcdeq0  12549  rppwr  12600  uzwodc  12609  algfx  12625  eucalgcvga  12631  lcmmndc  12635  lcmeq0  12644  qredeq  12669  isprm3  12691  rpexp  12726  sqpweven  12748  2sqpwodd  12749  phicl2  12787  phibnd  12790  phiprmpw  12795  fermltl  12807  pythagtriplem4  12842  pythagtriplem6  12844  pythagtriplem7  12845  pythagtriplem12  12849  pythagtriplem13  12850  pythagtriplem14  12851  pythagtriplem16  12853  pcdvdsb  12894  pc2dvds  12904  difsqpwdvds  12912  pcmpt  12917  pcmptdvds  12919  fldivp1  12922  prmpwdvds  12929  infpnlem1  12933  1arith  12941  4sqlem11  12975  ennnfonelemk  13022  ennnfonelemhom  13037  ennnfonelemrnh  13038  ennnfonelemf1  13040  ctinf  13052  ctiunctlemudc  13059  ctiunctlemf  13060  nninfdclemp1  13072  strslfvd  13125  strslfv2d  13126  strslssd  13130  imasival  13390  imasbas  13391  imasplusg  13392  imasaddfnlemg  13398  imasaddvallemg  13399  qusaddvallemg  13417  qusaddflemg  13418  qusaddval  13419  qusaddf  13420  qusmulval  13421  qusmulf  13422  lidrididd  13466  gsumfzval  13475  sgrpidmndm  13504  gsumfzz  13579  qusgrp2  13701  mulgnegnn  13720  eqgen  13815  rinvmod  13897  gsumfzconst  13929  qusrng  13973  srgdilem  13984  ringdilem  14027  qusring2  14081  lssintclm  14400  gsumfzfsumlemm  14603  mplsubgfilemm  14714  eltg3  14783  iuncld  14841  cnss2  14953  txcnp  14997  uptx  15000  xblm  15143  metss  15220  fsumcncntop  15293  rescncf  15307  dedekindeulemlu  15347  suplociccex  15351  dedekindicclemlu  15356  dedekindicc  15359  ivthdec  15370  limccnp2lem  15402  dvaddxx  15429  dvmulxx  15430  dvrecap  15439  reeff1olem  15497  perfectlem2  15726  lgsval  15735  lgsfvalg  15736  lgsfcl2  15737  lgscllem  15738  lgsval2lem  15741  lgsneg  15755  lgsdir2  15764  lgsdir  15766  lgsdi  15768  lgsne0  15769  lgsdirnn0  15778  lgsdinn0  15779  gausslemma2dlem0c  15782  m1lgs  15816  2lgslem1  15822  2lgs  15835  2lgsoddprm  15844  2sqlem6  15851  incistruhgr  15943  upgredg  15997  uhgr2edg  16059  usgriedgdomord  16078  wlkpropg  16177  wlkvtxeledgg  16197  wlk2f  16204  clwwlknonccat  16286  clwwlknonex2lem2  16291  sumdc2  16398  pwle2  16602  subctctexmid  16604  nninfsellemeq  16619  nnnninfex  16627  exmidsbthrlem  16629  cndcap  16666  gfsump1  16689