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  2754  elex2  2755  spcimdv  2823  spcimedv  2825  spcedv  2828  rspcdva  2848  elabd  2884  spsbcd  2977  opth  4239  euotd  4256  ssorduni  4488  tfisi  4588  omsinds  4623  nnpredcl  4624  sotri2  5028  sotri3  5029  unielrel  5158  funmo  5233  fnfvima  5753  fliftfun  5799  fliftval  5803  riota5f  5857  riotass2  5859  oprssdmm  6174  tfrlem5  6317  tfrlemibxssdm  6330  tfrlemibfn  6331  tfrlemiex  6334  tfr1onlemsucfn  6343  tfr1onlemsucaccv  6344  tfr1onlembxssdm  6346  tfr1onlembfn  6347  tfr1onlemex  6350  tfr1onlemres  6352  tfrcllemsucfn  6356  tfrcllemsucaccv  6357  tfrcllembxssdm  6359  tfrcllembfn  6360  tfrcllemex  6363  tfrcllemres  6365  tfrcl  6367  rdgisucinc  6388  frecabex  6401  frecabcl  6402  nntr2  6506  ertr  6552  qliftlem  6615  th3q  6642  resixp  6735  f1dom2g  6758  dom3d  6776  en1  6801  xpdom3m  6836  xpf1o  6846  phplem4dom  6864  phpm  6867  phpelm  6868  findcard  6890  finexdc  6904  fiintim  6930  fisseneq  6933  ssfirab  6935  f1dmvrnfibi  6945  iunfidisj  6947  fidcenumlemrk  6955  dcfi  6982  suplub2ti  7002  supelti  7003  ordiso2  7036  caseinl  7092  caseinr  7093  djudom  7094  difinfsn  7101  difinfinf  7102  ctm  7110  enumct  7116  nnnninfeq  7128  ismkvnex  7155  exmidfodomrlemr  7203  exmidfodomrlemrALT  7204  acfun  7208  exmidontriimlem2  7223  exmidontriimlem3  7224  exmidapne  7261  cc2lem  7267  cc3  7269  recexnq  7391  ltbtwnnqq  7416  addnnnq0  7450  mulnnnq0  7451  prarloclemn  7500  prarloc  7504  distrlem1prl  7583  distrlem1pru  7584  distrlem4prl  7585  distrlem4pru  7586  ltexprlemrl  7611  cauappcvgprlemladdru  7657  cauappcvgprlemladdrl  7658  addsrpr  7746  mulsrpr  7747  map2psrprg  7806  axpre-suploclemres  7902  lemul12a  8821  lemulge11  8825  sup3exmid  8916  nngt0  8946  nn0ge0  9203  nn0ge2m1nn  9238  zletric  9299  zlelttric  9300  nn0n0n1ge2b  9334  nn0ind-raph  9372  supinfneg  9597  infsupneg  9598  infregelbex  9600  rpge0  9668  fz0fzelfz0  10129  fz0fzdiffz0  10132  ige2m2fzo  10200  elfzodifsumelfzo  10203  elfzom1elp1fzo  10204  exfzdc  10242  qletric  10246  qlelttric  10247  rebtwn2zlemshrink  10256  frecuzrdgtcl  10414  frecuzrdg0  10415  frecuzrdgfunlem  10421  frecuzrdg0t  10424  frecuzrdgsuctlem  10425  frecfzennn  10428  seq3f1olemstep  10503  expcl2lemap  10534  leexp1a  10577  expnbnd  10646  faclbnd  10723  faclbnd6  10726  facavg  10728  fihasheqf1oi  10769  fihashf1rn  10770  fihashss  10798  fiubm  10810  seq3coll  10824  resqrexlemdecn  11023  qabsor  11086  cau3lem  11125  xrmaxiflemab  11257  xrmaxadd  11271  climcn2  11319  sumeq2  11369  sumrbdclem  11387  summodclem3  11390  summodclem2a  11391  zsumdc  11394  fsumgcl  11396  fsum3  11397  isumss  11401  fsumadd  11416  fsum2dlemstep  11444  fisum0diag2  11457  fsummulc2  11458  modfsummodlemstep  11467  fsumabs  11475  fsumrelem  11481  fsumiun  11487  isumshft  11500  mertenslem2  11546  prodeq2  11567  prodrbdclem  11581  prodmodclem3  11585  prodmodclem2a  11586  zproddc  11589  fprodseq  11593  fprodmul  11601  fprodconst  11630  fprodap0  11631  fprod2dlemstep  11632  fprodrec  11639  fprodsplit1f  11644  fprodap0f  11646  fprodle  11650  sin02gt0  11773  efieq1re  11781  p1modz1  11803  dvdsleabs2  11854  4dvdseven  11924  gcdmndc  11947  zsupcllemstep  11948  infssuzex  11952  gcdsupex  11960  gcdsupcl  11961  gcdeq0  11980  gcdaddm  11987  rppwr  12031  uzwodc  12040  nnwosdc  12042  algfx  12054  eucalgcvga  12060  lcmmndc  12064  lcmval  12065  lcmcllem  12069  lcmledvds  12072  lcmeq0  12073  qredeq  12098  isprm3  12120  prmdc  12132  rpexp  12155  sqpweven  12177  2sqpwodd  12178  phicl2  12216  phibnd  12219  phiprmpw  12224  fermltl  12236  pythagtriplem4  12270  pythagtriplem6  12272  pythagtriplem7  12273  pythagtriplem12  12277  pythagtriplem13  12278  pythagtriplem14  12279  pythagtriplem16  12281  pclemdc  12290  pcdvdsb  12321  pc2dvds  12331  difsqpwdvds  12339  pcmpt  12343  pcmptdvds  12345  fldivp1  12348  prmpwdvds  12355  infpnlem1  12359  infpnlem2  12360  1arith  12367  ennnfonelemk  12403  ennnfonelemhom  12418  ennnfonelemrnh  12419  ennnfonelemf1  12421  ctinf  12433  ctiunctlemudc  12440  ctiunctlemf  12441  nninfdclemcl  12451  nninfdclemp1  12453  strslfvd  12506  strslfv2d  12507  strslssd  12511  imasival  12732  imasbas  12733  imasplusg  12734  imasaddfnlemg  12740  imasaddvallemg  12741  qusaddvallemg  12757  qusaddflemg  12758  qusaddval  12759  qusaddf  12760  qusmulval  12761  qusmulf  12762  lidrididd  12806  sgrpidmndm  12826  mulgnegnn  12998  eqgen  13091  rinvmod  13117  srgdilem  13157  ringdilem  13200  lssintclm  13476  eltg3  13642  iuncld  13700  cnss2  13812  txcnp  13856  uptx  13859  xblm  14002  metss  14079  fsumcncntop  14141  rescncf  14153  dedekindeulemlu  14184  suplociccex  14188  dedekindicclemlu  14193  dedekindicc  14196  ivthdec  14207  limccnp2lem  14230  dvaddxx  14252  dvmulxx  14253  dvrecap  14262  reeff1olem  14277  lgsval  14490  lgsfvalg  14491  lgsfcl2  14492  lgscllem  14493  lgsval2lem  14496  lgsneg  14510  lgsdir2  14519  lgsdir  14521  lgsdi  14523  lgsne0  14524  lgsdirnn0  14533  lgsdinn0  14534  m1lgs  14537  2sqlem6  14552  sumdc2  14636  pwle2  14833  subctctexmid  14835  nninfsellemeq  14848  exmidsbthrlem  14855  cndcap  14892