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  654  jcnd  656  annimdc  943  pm4.55dc  944  orandc  945  dn1dc  966  syl2an23an  1333  xordidc  1441  nfimd  1631  exlimd2  1641  elex22  2815  elex2  2816  spcimdv  2887  spcimedv  2889  spcedv  2892  rspcdva  2912  elabd  2948  spsbcd  3041  opth  4323  euotd  4341  ssorduni  4579  tfisi  4679  omsinds  4714  nnpredcl  4715  sotri2  5126  sotri3  5127  unielrel  5256  funmo  5333  fnfvima  5878  resfvresima  5880  fliftfun  5926  fliftval  5930  riota5f  5987  riotass2  5989  fovcld  6115  oprssdmm  6323  tfrlem5  6466  tfrlemibxssdm  6479  tfrlemibfn  6480  tfrlemiex  6483  tfr1onlemsucfn  6492  tfr1onlemsucaccv  6493  tfr1onlembxssdm  6495  tfr1onlembfn  6496  tfr1onlemex  6499  tfr1onlemres  6501  tfrcllemsucfn  6505  tfrcllemsucaccv  6506  tfrcllembxssdm  6508  tfrcllembfn  6509  tfrcllemex  6512  tfrcllemres  6514  tfrcl  6516  rdgisucinc  6537  frecabex  6550  frecabcl  6551  nntr2  6657  ertr  6703  qliftlem  6768  th3q  6795  resixp  6888  f1dom2g  6915  dom3d  6933  domssr  6937  en1  6959  xpdom3m  7001  xpf1o  7013  phplem4dom  7031  phpm  7035  phpelm  7036  findcard  7058  finexdc  7073  fiintim  7104  fisseneq  7107  ssfirab  7109  opabfi  7111  f1dmvrnfibi  7122  iunfidisj  7124  fidcenumlemrk  7132  dcfi  7159  suplub2ti  7179  supelti  7180  ordiso2  7213  caseinl  7269  caseinr  7270  djudom  7271  difinfsn  7278  difinfinf  7279  ctm  7287  enumct  7293  nnnninfeq  7306  ismkvnex  7333  exmidfodomrlemr  7391  exmidfodomrlemrALT  7392  acfun  7400  exmidontriimlem2  7415  exmidontriimlem3  7416  exmidapne  7457  cc2lem  7463  cc3  7465  recexnq  7588  ltbtwnnqq  7613  addnnnq0  7647  mulnnnq0  7648  prarloclemn  7697  prarloc  7701  distrlem1prl  7780  distrlem1pru  7781  distrlem4prl  7782  distrlem4pru  7783  ltexprlemrl  7808  cauappcvgprlemladdru  7854  cauappcvgprlemladdrl  7855  addsrpr  7943  mulsrpr  7944  map2psrprg  8003  axpre-suploclemres  8099  lemul12a  9020  lemulge11  9024  sup3exmid  9115  nngt0  9146  nn0ge0  9405  nn0ge2m1nn  9440  zletric  9501  zlelttric  9502  nn0n0n1ge2b  9537  nn0ind-raph  9575  supinfneg  9802  infsupneg  9803  infregelbex  9805  rpge0  9874  fz0fzelfz0  10335  fz0fzdiffz0  10338  ige2m2fzo  10416  elfzodifsumelfzo  10419  elfzom1elp1fzo  10420  exfzdc  10458  zsupcllemstep  10461  infssuzex  10465  qletric  10473  qlelttric  10474  rebtwn2zlemshrink  10485  frecuzrdgtcl  10646  frecuzrdg0  10647  frecuzrdgfunlem  10653  frecuzrdg0t  10656  frecuzrdgsuctlem  10657  frecfzennn  10660  seq3f1olemstep  10748  expcl2lemap  10785  leexp1a  10828  expnbnd  10897  faclbnd  10975  faclbnd6  10978  facavg  10980  fihasheqf1oi  11021  fihashf1rn  11022  fihashss  11051  fiubm  11063  seq3coll  11077  wrdsymb0  11117  wrdlenge2n0  11120  ccatsymb  11150  pfxnd  11237  pfxccat1  11250  swrdpfx  11255  pfxpfx  11256  wrd2ind  11271  pfxccatin12  11281  pfxccat3  11282  swrdccat  11283  pfxccatpfx1  11284  pfxccatpfx2  11285  swrdccatin1d  11291  pfxccatin12d  11293  resqrexlemdecn  11539  qabsor  11602  cau3lem  11641  xrmaxiflemab  11774  xrmaxadd  11788  climcn2  11836  sumeq2  11886  sumrbdclem  11904  summodclem3  11907  summodclem2a  11908  zsumdc  11911  fsumgcl  11913  fsum3  11914  isumss  11918  fsumadd  11933  fsum2dlemstep  11961  fisum0diag2  11974  fsummulc2  11975  modfsummodlemstep  11984  fsumabs  11992  fsumrelem  11998  fsumiun  12004  isumshft  12017  mertenslem2  12063  prodeq2  12084  prodrbdclem  12098  prodmodclem3  12102  prodmodclem2a  12103  zproddc  12106  fprodseq  12110  fprodmul  12118  fprodconst  12147  fprodap0  12148  fprod2dlemstep  12149  fprodrec  12156  fprodsplit1f  12161  fprodap0f  12163  fprodle  12167  sin02gt0  12291  efieq1re  12299  p1modz1  12321  dvdsleabs2  12373  4dvdseven  12444  bitsfzo  12482  bitsinv1lem  12488  gcdeq0  12514  rppwr  12565  uzwodc  12574  algfx  12590  eucalgcvga  12596  lcmmndc  12600  lcmeq0  12609  qredeq  12634  isprm3  12656  rpexp  12691  sqpweven  12713  2sqpwodd  12714  phicl2  12752  phibnd  12755  phiprmpw  12760  fermltl  12772  pythagtriplem4  12807  pythagtriplem6  12809  pythagtriplem7  12810  pythagtriplem12  12814  pythagtriplem13  12815  pythagtriplem14  12816  pythagtriplem16  12818  pcdvdsb  12859  pc2dvds  12869  difsqpwdvds  12877  pcmpt  12882  pcmptdvds  12884  fldivp1  12887  prmpwdvds  12894  infpnlem1  12898  1arith  12906  4sqlem11  12940  ennnfonelemk  12987  ennnfonelemhom  13002  ennnfonelemrnh  13003  ennnfonelemf1  13005  ctinf  13017  ctiunctlemudc  13024  ctiunctlemf  13025  nninfdclemp1  13037  strslfvd  13090  strslfv2d  13091  strslssd  13095  imasival  13355  imasbas  13356  imasplusg  13357  imasaddfnlemg  13363  imasaddvallemg  13364  qusaddvallemg  13382  qusaddflemg  13383  qusaddval  13384  qusaddf  13385  qusmulval  13386  qusmulf  13387  lidrididd  13431  gsumfzval  13440  sgrpidmndm  13469  gsumfzz  13544  qusgrp2  13666  mulgnegnn  13685  eqgen  13780  rinvmod  13862  gsumfzconst  13894  qusrng  13937  srgdilem  13948  ringdilem  13991  qusring2  14045  lssintclm  14364  gsumfzfsumlemm  14567  mplsubgfilemm  14678  eltg3  14747  iuncld  14805  cnss2  14917  txcnp  14961  uptx  14964  xblm  15107  metss  15184  fsumcncntop  15257  rescncf  15271  dedekindeulemlu  15311  suplociccex  15315  dedekindicclemlu  15320  dedekindicc  15323  ivthdec  15334  limccnp2lem  15366  dvaddxx  15393  dvmulxx  15394  dvrecap  15403  reeff1olem  15461  perfectlem2  15690  lgsval  15699  lgsfvalg  15700  lgsfcl2  15701  lgscllem  15702  lgsval2lem  15705  lgsneg  15719  lgsdir2  15728  lgsdir  15730  lgsdi  15732  lgsne0  15733  lgsdirnn0  15742  lgsdinn0  15743  gausslemma2dlem0c  15746  m1lgs  15780  2lgslem1  15786  2lgs  15799  2lgsoddprm  15808  2sqlem6  15815  incistruhgr  15906  upgredg  15958  uhgr2edg  16020  usgriedgdomord  16039  wlkpropg  16070  wlkvtxeledgg  16090  wlk2f  16097  sumdc2  16246  pwle2  16451  subctctexmid  16453  nninfsellemeq  16468  nnnninfex  16476  exmidsbthrlem  16478  cndcap  16515