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  415  jc  660  jcnd  662  annimdc  950  pm4.55dc  951  orandc  952  dn1dc  973  syl2an23an  1340  xordidc  1448  nfimd  1638  exlimd2  1648  elex22  2837  elex2  2838  spcimdv  2909  spcimedv  2911  spcedv  2914  rspcdva  2934  elabd  2971  spsbcd  3064  ifeqeqxdc  3687  opth  4375  euotd  4393  ssorduni  4632  tfisi  4732  omsinds  4767  nnpredcl  4768  sotri2  5183  sotri3  5184  unielrel  5313  funmo  5390  fnfvima  5946  resfvresima  5949  fliftfun  5995  fliftval  5999  riota5f  6058  riotass2  6060  fovcld  6186  oprssdmm  6398  funsssuppss  6491  tfrlem5  6578  tfrlemibxssdm  6591  tfrlemibfn  6592  tfrlemiex  6595  tfr1onlemsucfn  6604  tfr1onlemsucaccv  6605  tfr1onlembxssdm  6607  tfr1onlembfn  6608  tfr1onlemex  6611  tfr1onlemres  6613  tfrcllemsucfn  6617  tfrcllemsucaccv  6618  tfrcllembxssdm  6620  tfrcllembfn  6621  tfrcllemex  6624  tfrcllemres  6626  tfrcl  6628  rdgisucinc  6649  frecabex  6662  frecabcl  6663  nntr2  6769  ertr  6815  qliftlem  6880  th3q  6907  resixp  7008  f1dom2g  7035  dom3d  7053  domssr  7057  en1  7079  xpdom3m  7125  xpf1o  7137  phplem4dom  7156  phpm  7160  phpelm  7161  findcard  7185  finexdc  7200  fiintim  7231  fisseneq  7235  ssfirab  7237  opabfi  7240  f1dmvrnfibi  7251  iunfidisj  7253  fidcenumlemrk  7264  dcfi  7308  fdcf1  7309  2omapfi  7313  suplub2ti  7334  supelti  7335  ordiso2  7368  caseinl  7424  caseinr  7425  djudom  7426  difinfsn  7433  difinfinf  7434  ctm  7442  enumct  7448  nnnninfeq  7461  ismkvnex  7488  exmidfodomrlemr  7547  exmidfodomrlemrALT  7548  acfun  7556  exmidontriimlem2  7571  exmidontriimlem3  7572  exmidapne  7619  cc2lem  7625  cc3  7627  recexnq  7750  ltbtwnnqq  7775  addnnnq0  7809  mulnnnq0  7810  prarloclemn  7859  prarloc  7863  distrlem1prl  7942  distrlem1pru  7943  distrlem4prl  7944  distrlem4pru  7945  ltexprlemrl  7970  cauappcvgprlemladdru  8016  cauappcvgprlemladdrl  8017  addsrpr  8105  mulsrpr  8106  map2psrprg  8165  axpre-suploclemres  8261  lemul12a  9185  lemulge11  9189  sup3exmid  9280  nngt0  9311  nn0ge0  9570  nn0ge2m1nn  9609  zletric  9670  zlelttric  9671  nn0n0n1ge2b  9707  nn0ind-raph  9745  supinfneg  9977  infsupneg  9978  infregelbex  9980  rpge0  10049  fz0fzelfz0  10515  fz0fzdiffz0  10518  ige2m2fzo  10597  elfzodifsumelfzo  10600  elfzom1elp1fzo  10601  exfzdc  10640  zsupcllemstep  10643  infssuzex  10647  qletric  10657  qlelttric  10658  rebtwn2zlemshrink  10669  frecuzrdgtcl  10830  frecuzrdg0  10831  frecuzrdgfunlem  10837  frecuzrdg0t  10840  frecuzrdgsuctlem  10841  frecfzennn  10844  seq3f1olemstep  10932  expcl2lemap  10969  leexp1a  11012  expnbnd  11082  faclbnd  11160  faclbnd6  11163  facavg  11165  fihasheqf1oi  11207  fihashf1rn  11208  fihashss  11238  fiubm  11252  seq3coll  11275  wrdsymb0  11318  wrdlenge2n0  11321  ccatsymb  11351  pfxnd  11442  pfxccat1  11455  swrdpfx  11460  pfxpfx  11461  wrd2ind  11476  pfxccatin12  11486  pfxccat3  11487  swrdccat  11488  pfxccatpfx1  11489  pfxccatpfx2  11490  swrdccatin1d  11496  pfxccatin12d  11498  resqrexlemdecn  11759  qabsor  11822  cau3lem  11861  xrmaxiflemab  11994  xrmaxadd  12008  climcn2  12056  sumeq2  12106  sumrbdclem  12125  summodclem3  12128  summodclem2a  12129  zsumdc  12132  fsumgcl  12134  fsum3  12135  isumss  12139  fsumadd  12154  fsum2dlemstep  12182  fisum0diag2  12195  fsummulc2  12196  modfsummodlemstep  12205  fsumabs  12213  fsumrelem  12219  fsumiun  12225  isumshft  12238  mertenslem2  12284  prodeq2  12305  prodrbdclem  12319  prodmodclem3  12323  prodmodclem2a  12324  zproddc  12327  fprodseq  12331  fprodmul  12339  fprodconst  12368  fprodap0  12369  fprod2dlemstep  12370  fprodrec  12377  fprodsplit1f  12382  fprodap0f  12384  fprodle  12388  sin02gt0  12512  efieq1re  12520  p1modz1  12542  dvdsleabs2  12594  4dvdseven  12665  bitsfzo  12703  bitsinv1lem  12709  gcdeq0  12735  rppwr  12786  uzwodc  12795  algfx  12811  eucalgcvga  12817  lcmmndc  12821  lcmeq0  12830  qredeq  12855  isprm3  12877  rpexp  12912  sqpweven  12934  2sqpwodd  12935  phicl2  12973  phibnd  12976  phiprmpw  12981  fermltl  12993  pythagtriplem4  13028  pythagtriplem6  13030  pythagtriplem7  13031  pythagtriplem12  13035  pythagtriplem13  13036  pythagtriplem14  13037  pythagtriplem16  13039  pcdvdsb  13080  pc2dvds  13090  difsqpwdvds  13098  pcmpt  13103  pcmptdvds  13105  fldivp1  13108  prmpwdvds  13115  infpnlem1  13119  1arith  13127  4sqlem11  13161  ballotfilemfp1  13212  ballotfilemic  13231  ennnfonelemk  13272  ennnfonelemhom  13287  ennnfonelemrnh  13288  ennnfonelemf1  13290  ctinf  13302  ctiunctlemudc  13309  ctiunctlemf  13310  nninfdclemp1  13322  strslfvd  13375  strslfv2d  13376  strslssd  13380  imasival  13607  imasbas  13608  imasplusg  13609  imasaddfnlemg  13615  imasaddvallemg  13616  qusaddvallemg  13634  qusaddflemg  13635  qusaddval  13636  qusaddf  13637  qusmulval  13638  qusmulf  13639  lidrididd  13682  gzsumfzval  13691  sgrpidmndm  13713  qusgrp2  13896  mulgnegnn  13915  eqgen  14010  rinvmod  14093  gzsumconst  14123  gsump1  14137  gsummptfidmadd  14141  qusrng  14235  srgdilem  14250  ringdilem  14293  qusring2  14347  lssintclm  14696  mplsubgfilemm  15015  eltg3  15084  iuncld  15142  cnss2  15254  txcnp  15298  uptx  15301  xblm  15444  metss  15521  fsumcncntop  15594  rescncf  15608  dedekindeulemlu  15648  suplociccex  15652  dedekindicclemlu  15657  dedekindicc  15660  ivthdec  15671  limccnp2lem  15703  dvaddxx  15730  dvmulxx  15731  dvrecap  15740  reeff1olem  15798  perfectlem2  16031  lgsval  16040  lgsfvalg  16041  lgsfcl2  16042  lgscllem  16043  lgsval2lem  16046  lgsneg  16060  lgsdir2  16069  lgsdir  16071  lgsdi  16073  lgsne0  16074  lgsdirnn0  16083  lgsdinn0  16084  gausslemma2dlem0c  16087  m1lgs  16121  2lgslem1  16127  2lgs  16140  2lgsoddprm  16149  2sqlem6  16156  incistruhgr  16248  upgredg  16302  uhgr2edg  16364  usgriedgdomord  16383  wlkpropg  16482  wlkvtxeledgg  16502  wlk2f  16509  clwwlknonccat  16591  clwwlknonex2lem2  16596  eupth2lem3lem4fi  16631  eupth2lem3lem7fi  16632  dichmul0orlem3  16672  sumdc2  16744  pwle2  16945  subctctexmid  16947  nninfsellemeq  16965  nnnninfex  16973  exmidsbthrlem  16975  cndcap  17017