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 )

This proof depends on syntax axioms:   -> wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used 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  4377  euotd  4395  ssorduni  4634  tfisi  4734  omsinds  4769  nnpredcl  4770  sotri2  5185  sotri3  5186  unielrel  5315  funmo  5392  fnfvima  5953  resfvresima  5956  fliftfun  6002  fliftval  6006  riota5f  6065  riotass2  6067  fovcld  6193  oprssdmm  6405  funsssuppss  6498  tfrlem5  6585  tfrlemibxssdm  6598  tfrlemibfn  6599  tfrlemiex  6602  tfr1onlemsucfn  6611  tfr1onlemsucaccv  6612  tfr1onlembxssdm  6614  tfr1onlembfn  6615  tfr1onlemex  6618  tfr1onlemres  6620  tfrcllemsucfn  6624  tfrcllemsucaccv  6625  tfrcllembxssdm  6627  tfrcllembfn  6628  tfrcllemex  6631  tfrcllemres  6633  tfrcl  6635  rdgisucinc  6656  frecabex  6669  frecabcl  6670  nntr2  6776  ertr  6822  qliftlem  6887  th3q  6914  resixp  7015  f1dom2g  7042  dom3d  7060  domssr  7064  en1  7086  xpdom3m  7132  xpf1o  7144  phplem4dom  7163  phpm  7167  phpelm  7168  findcard  7192  finexdc  7207  fiintim  7238  fisseneq  7242  ssfirab  7244  opabfi  7247  f1dmvrnfibi  7258  iunfidisj  7260  fidcenumlemrk  7271  dcfi  7315  fdcf1  7316  2omapfi  7320  suplub2ti  7341  supelti  7342  ordiso2  7375  caseinl  7431  caseinr  7432  djudom  7433  difinfsn  7440  difinfinf  7441  ctm  7449  enumct  7455  nnnninfeq  7468  ismkvnex  7495  exmidfodomrlemr  7554  exmidfodomrlemrALT  7555  acfun  7563  exmidontriimlem2  7578  exmidontriimlem3  7579  exmidapne  7626  cc2lem  7632  cc3  7634  recexnq  7757  ltbtwnnqq  7782  addnnnq0  7816  mulnnnq0  7817  prarloclemn  7866  prarloc  7870  distrlem1prl  7949  distrlem1pru  7950  distrlem4prl  7951  distrlem4pru  7952  ltexprlemrl  7977  cauappcvgprlemladdru  8023  cauappcvgprlemladdrl  8024  addsrpr  8112  mulsrpr  8113  map2psrprg  8172  axpre-suploclemres  8268  lemul12a  9192  lemulge11  9196  sup3exmid  9287  nngt0  9329  nn0ge0  9588  nn0ge2m1nn  9627  zletric  9688  zlelttric  9689  nn0n0n1ge2b  9725  nn0ind-raph  9763  supinfneg  9995  infsupneg  9996  infregelbex  9998  rpge0  10067  fz0fzelfz0  10534  fz0fzdiffz0  10537  ige2m2fzo  10616  elfzodifsumelfzo  10619  elfzom1elp1fzo  10620  exfzdc  10659  zsupcllemstep  10662  infssuzex  10666  qletric  10676  qlelttric  10677  rebtwn2zlemshrink  10688  frecuzrdgtcl  10849  frecuzrdg0  10850  frecuzrdgfunlem  10856  frecuzrdg0t  10859  frecuzrdgsuctlem  10860  frecfzennn  10863  seq3f1olemstep  10951  expcl2lemap  10988  leexp1a  11031  expnbnd  11101  faclbnd  11179  faclbnd6  11182  facavg  11184  fihasheqf1oi  11226  fihashf1rn  11227  fihashss  11257  fiubm  11271  seq3coll  11294  wrdsymb0  11337  wrdlenge2n0  11340  ccatsymb  11370  pfxnd  11461  pfxccat1  11474  swrdpfx  11479  pfxpfx  11480  wrd2ind  11495  pfxccatin12  11505  pfxccat3  11506  swrdccat  11507  pfxccatpfx1  11508  pfxccatpfx2  11509  swrdccatin1d  11515  pfxccatin12d  11517  resqrexlemdecn  11778  qabsor  11841  cau3lem  11880  xrmaxiflemab  12013  xrmaxadd  12027  climcn2  12075  sumeq2  12125  sumrbdclem  12144  summodclem3  12147  summodclem2a  12148  zsumdc  12151  fsumgcl  12153  fsum3  12154  isumss  12158  fsumadd  12173  fsum2dlemstep  12201  fisum0diag2  12214  fsummulc2  12215  modfsummodlemstep  12224  fsumabs  12232  fsumrelem  12238  fsumiun  12244  isumshft  12257  mertenslem2  12303  prodeq2  12324  prodrbdclem  12338  prodmodclem3  12342  prodmodclem2a  12343  zproddc  12346  fprodseq  12350  fprodmul  12358  fprodconst  12387  fprodap0  12388  fprod2dlemstep  12389  fprodrec  12396  fprodsplit1f  12401  fprodap0f  12403  fprodle  12407  sin02gt0  12531  efieq1re  12539  p1modz1  12561  dvdsleabs2  12613  4dvdseven  12684  bitsfzo  12722  bitsinv1lem  12728  gcdeq0  12754  rppwr  12805  uzwodc  12814  algfx  12830  eucalgcvga  12836  lcmmndc  12840  lcmeq0  12849  qredeq  12874  isprm3  12896  rpexp  12931  sqpweven  12953  2sqpwodd  12954  phicl2  12992  phibnd  12995  phiprmpw  13000  fermltl  13012  pythagtriplem4  13047  pythagtriplem6  13049  pythagtriplem7  13050  pythagtriplem12  13054  pythagtriplem13  13055  pythagtriplem14  13056  pythagtriplem16  13058  pcdvdsb  13099  pc2dvds  13109  difsqpwdvds  13117  pcmpt  13122  pcmptdvds  13124  fldivp1  13127  prmpwdvds  13134  infpnlem1  13138  1arith  13146  4sqlem11  13180  ballotfilemfp1  13231  ballotfilemic  13250  ennnfonelemk  13291  ennnfonelemhom  13306  ennnfonelemrnh  13307  ennnfonelemf1  13309  ctinf  13321  ctiunctlemudc  13328  ctiunctlemf  13329  nninfdclemp1  13341  strslfvd  13394  strslfv2d  13395  strslssd  13399  imasival  13627  imasbas  13628  imasplusg  13629  imasaddfnlemg  13635  imasaddvallemg  13636  qusaddvallemg  13654  qusaddflemg  13655  qusaddval  13656  qusaddf  13657  qusmulval  13658  qusmulf  13659  lidrididd  13702  gzsumfzval  13711  sgrpidmndm  13733  qusgrp2  13916  mulgnegnn  13935  eqgen  14030  rinvmod  14113  gzsumconst  14143  gsump1  14157  gsummptfidmadd  14161  qusrng  14257  srgdilem  14273  ringdilem  14316  qusring2  14371  lssintclm  14721  mplsubgfilemm  15089  eltg3  15158  iuncld  15216  cnss2  15328  txcnp  15372  uptx  15375  xblm  15518  metss  15595  fsumcncntop  15668  rescncf  15682  dedekindeulemlu  15722  suplociccex  15726  dedekindicclemlu  15731  dedekindicc  15734  ivthdec  15745  limccnp2lem  15777  dvaddxx  15804  dvmulxx  15805  dvrecap  15814  reeff1olem  15872  perfectlem2  16114  lgsval  16123  lgsfvalg  16124  lgsfcl2  16125  lgscllem  16126  lgsval2lem  16129  lgsneg  16143  lgsdir2  16152  lgsdir  16154  lgsdi  16156  lgsne0  16157  lgsdirnn0  16166  lgsdinn0  16167  gausslemma2dlem0c  16170  m1lgs  16204  2lgslem1  16210  2lgs  16223  2lgsoddprm  16232  2sqlem6  16239  incistruhgr  16331  upgredg  16385  uhgr2edg  16447  usgriedgdomord  16466  wlkpropg  16565  wlkvtxeledgg  16585  wlk2f  16592  clwwlknonccat  16674  clwwlknonex2lem2  16679  eupth2lem3lem4fi  16714  eupth2lem3lem7fi  16715  dichmul0orlem3  16755  sumdc2  16827  pwle2  17028  subctctexmid  17030  nninfsellemeq  17057  nnnninfex  17065  exmidsbthrlem  17067  cndcap  17109