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  650  jcnd  652  annimdc  937  orandc  939  dn1dc  960  syl2an23an  1299  xordidc  1399  nfimd  1585  exlimd2  1595  elex22  2753  elex2  2754  spcimdv  2822  spcimedv  2824  spcedv  2827  rspcdva  2847  elabd  2883  spsbcd  2976  opth  4238  euotd  4255  ssorduni  4487  tfisi  4587  omsinds  4622  nnpredcl  4623  sotri2  5027  sotri3  5028  unielrel  5157  funmo  5232  fnfvima  5752  fliftfun  5797  fliftval  5801  riota5f  5855  riotass2  5857  oprssdmm  6172  tfrlem5  6315  tfrlemibxssdm  6328  tfrlemibfn  6329  tfrlemiex  6332  tfr1onlemsucfn  6341  tfr1onlemsucaccv  6342  tfr1onlembxssdm  6344  tfr1onlembfn  6345  tfr1onlemex  6348  tfr1onlemres  6350  tfrcllemsucfn  6354  tfrcllemsucaccv  6355  tfrcllembxssdm  6357  tfrcllembfn  6358  tfrcllemex  6361  tfrcllemres  6363  tfrcl  6365  rdgisucinc  6386  frecabex  6399  frecabcl  6400  nntr2  6504  ertr  6550  qliftlem  6613  th3q  6640  resixp  6733  f1dom2g  6756  dom3d  6774  en1  6799  xpdom3m  6834  xpf1o  6844  phplem4dom  6862  phpm  6865  phpelm  6866  findcard  6888  finexdc  6902  fiintim  6928  fisseneq  6931  ssfirab  6933  f1dmvrnfibi  6943  iunfidisj  6945  fidcenumlemrk  6953  dcfi  6980  suplub2ti  7000  supelti  7001  ordiso2  7034  caseinl  7090  caseinr  7091  djudom  7092  difinfsn  7099  difinfinf  7100  ctm  7108  enumct  7114  nnnninfeq  7126  ismkvnex  7153  exmidfodomrlemr  7201  exmidfodomrlemrALT  7202  acfun  7206  exmidontriimlem2  7221  exmidontriimlem3  7222  exmidapne  7259  cc2lem  7265  cc3  7267  recexnq  7389  ltbtwnnqq  7414  addnnnq0  7448  mulnnnq0  7449  prarloclemn  7498  prarloc  7502  distrlem1prl  7581  distrlem1pru  7582  distrlem4prl  7583  distrlem4pru  7584  ltexprlemrl  7609  cauappcvgprlemladdru  7655  cauappcvgprlemladdrl  7656  addsrpr  7744  mulsrpr  7745  map2psrprg  7804  axpre-suploclemres  7900  lemul12a  8819  lemulge11  8823  sup3exmid  8914  nngt0  8944  nn0ge0  9201  nn0ge2m1nn  9236  zletric  9297  zlelttric  9298  nn0n0n1ge2b  9332  nn0ind-raph  9370  supinfneg  9595  infsupneg  9596  infregelbex  9598  rpge0  9666  fz0fzelfz0  10127  fz0fzdiffz0  10130  ige2m2fzo  10198  elfzodifsumelfzo  10201  elfzom1elp1fzo  10202  exfzdc  10240  qletric  10244  qlelttric  10245  rebtwn2zlemshrink  10254  frecuzrdgtcl  10412  frecuzrdg0  10413  frecuzrdgfunlem  10419  frecuzrdg0t  10422  frecuzrdgsuctlem  10423  frecfzennn  10426  seq3f1olemstep  10501  expcl2lemap  10532  leexp1a  10575  expnbnd  10644  faclbnd  10721  faclbnd6  10724  facavg  10726  fihasheqf1oi  10767  fihashf1rn  10768  fihashss  10796  fiubm  10808  seq3coll  10822  resqrexlemdecn  11021  qabsor  11084  cau3lem  11123  xrmaxiflemab  11255  xrmaxadd  11269  climcn2  11317  sumeq2  11367  sumrbdclem  11385  summodclem3  11388  summodclem2a  11389  zsumdc  11392  fsumgcl  11394  fsum3  11395  isumss  11399  fsumadd  11414  fsum2dlemstep  11442  fisum0diag2  11455  fsummulc2  11456  modfsummodlemstep  11465  fsumabs  11473  fsumrelem  11479  fsumiun  11485  isumshft  11498  mertenslem2  11544  prodeq2  11565  prodrbdclem  11579  prodmodclem3  11583  prodmodclem2a  11584  zproddc  11587  fprodseq  11591  fprodmul  11599  fprodconst  11628  fprodap0  11629  fprod2dlemstep  11630  fprodrec  11637  fprodsplit1f  11642  fprodap0f  11644  fprodle  11648  sin02gt0  11771  efieq1re  11779  p1modz1  11801  dvdsleabs2  11852  4dvdseven  11922  gcdmndc  11945  zsupcllemstep  11946  infssuzex  11950  gcdsupex  11958  gcdsupcl  11959  gcdeq0  11978  gcdaddm  11985  rppwr  12029  uzwodc  12038  nnwosdc  12040  algfx  12052  eucalgcvga  12058  lcmmndc  12062  lcmval  12063  lcmcllem  12067  lcmledvds  12070  lcmeq0  12071  qredeq  12096  isprm3  12118  prmdc  12130  rpexp  12153  sqpweven  12175  2sqpwodd  12176  phicl2  12214  phibnd  12217  phiprmpw  12222  fermltl  12234  pythagtriplem4  12268  pythagtriplem6  12270  pythagtriplem7  12271  pythagtriplem12  12275  pythagtriplem13  12276  pythagtriplem14  12277  pythagtriplem16  12279  pclemdc  12288  pcdvdsb  12319  pc2dvds  12329  difsqpwdvds  12337  pcmpt  12341  pcmptdvds  12343  fldivp1  12346  prmpwdvds  12353  infpnlem1  12357  infpnlem2  12358  1arith  12365  ennnfonelemk  12401  ennnfonelemhom  12416  ennnfonelemrnh  12417  ennnfonelemf1  12419  ctinf  12431  ctiunctlemudc  12438  ctiunctlemf  12439  nninfdclemcl  12449  nninfdclemp1  12451  strslfvd  12504  strslfv2d  12505  strslssd  12509  imasival  12727  imasbas  12728  imasplusg  12729  imasaddfnlemg  12735  imasaddvallemg  12736  qusaddvallemg  12752  qusaddflemg  12753  qusaddval  12754  qusaddf  12755  qusmulval  12756  qusmulf  12757  lidrididd  12801  sgrpidmndm  12821  mulgnegnn  12993  eqgen  13086  rinvmod  13112  srgdilem  13152  ringdilem  13195  eltg3  13560  iuncld  13618  cnss2  13730  txcnp  13774  uptx  13777  xblm  13920  metss  13997  fsumcncntop  14059  rescncf  14071  dedekindeulemlu  14102  suplociccex  14106  dedekindicclemlu  14111  dedekindicc  14114  ivthdec  14125  limccnp2lem  14148  dvaddxx  14170  dvmulxx  14171  dvrecap  14180  reeff1olem  14195  lgsval  14408  lgsfvalg  14409  lgsfcl2  14410  lgscllem  14411  lgsval2lem  14414  lgsneg  14428  lgsdir2  14437  lgsdir  14439  lgsdi  14441  lgsne0  14442  lgsdirnn0  14451  lgsdinn0  14452  m1lgs  14455  2sqlem6  14470  sumdc2  14554  pwle2  14751  subctctexmid  14753  nninfsellemeq  14766  exmidsbthrlem  14773