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  651  jcnd  653  annimdc  939  pm4.55dc  940  orandc  941  dn1dc  962  syl2an23an  1310  xordidc  1410  nfimd  1599  exlimd2  1609  elex22  2778  elex2  2779  spcimdv  2848  spcimedv  2850  spcedv  2853  rspcdva  2873  elabd  2909  spsbcd  3002  opth  4270  euotd  4287  ssorduni  4523  tfisi  4623  omsinds  4658  nnpredcl  4659  sotri2  5067  sotri3  5068  unielrel  5197  funmo  5273  fnfvima  5797  fliftfun  5843  fliftval  5847  riota5f  5902  riotass2  5904  fovcld  6027  oprssdmm  6229  tfrlem5  6372  tfrlemibxssdm  6385  tfrlemibfn  6386  tfrlemiex  6389  tfr1onlemsucfn  6398  tfr1onlemsucaccv  6399  tfr1onlembxssdm  6401  tfr1onlembfn  6402  tfr1onlemex  6405  tfr1onlemres  6407  tfrcllemsucfn  6411  tfrcllemsucaccv  6412  tfrcllembxssdm  6414  tfrcllembfn  6415  tfrcllemex  6418  tfrcllemres  6420  tfrcl  6422  rdgisucinc  6443  frecabex  6456  frecabcl  6457  nntr2  6561  ertr  6607  qliftlem  6672  th3q  6699  resixp  6792  f1dom2g  6815  dom3d  6833  en1  6858  xpdom3m  6893  xpf1o  6905  phplem4dom  6923  phpm  6926  phpelm  6927  findcard  6949  finexdc  6963  fiintim  6992  fisseneq  6995  ssfirab  6997  opabfi  6999  f1dmvrnfibi  7010  iunfidisj  7012  fidcenumlemrk  7020  dcfi  7047  suplub2ti  7067  supelti  7068  ordiso2  7101  caseinl  7157  caseinr  7158  djudom  7159  difinfsn  7166  difinfinf  7167  ctm  7175  enumct  7181  nnnninfeq  7194  ismkvnex  7221  exmidfodomrlemr  7269  exmidfodomrlemrALT  7270  acfun  7274  exmidontriimlem2  7289  exmidontriimlem3  7290  exmidapne  7327  cc2lem  7333  cc3  7335  recexnq  7457  ltbtwnnqq  7482  addnnnq0  7516  mulnnnq0  7517  prarloclemn  7566  prarloc  7570  distrlem1prl  7649  distrlem1pru  7650  distrlem4prl  7651  distrlem4pru  7652  ltexprlemrl  7677  cauappcvgprlemladdru  7723  cauappcvgprlemladdrl  7724  addsrpr  7812  mulsrpr  7813  map2psrprg  7872  axpre-suploclemres  7968  lemul12a  8889  lemulge11  8893  sup3exmid  8984  nngt0  9015  nn0ge0  9274  nn0ge2m1nn  9309  zletric  9370  zlelttric  9371  nn0n0n1ge2b  9405  nn0ind-raph  9443  supinfneg  9669  infsupneg  9670  infregelbex  9672  rpge0  9741  fz0fzelfz0  10202  fz0fzdiffz0  10205  ige2m2fzo  10274  elfzodifsumelfzo  10277  elfzom1elp1fzo  10278  exfzdc  10316  zsupcllemstep  10319  infssuzex  10323  qletric  10331  qlelttric  10332  rebtwn2zlemshrink  10343  frecuzrdgtcl  10504  frecuzrdg0  10505  frecuzrdgfunlem  10511  frecuzrdg0t  10514  frecuzrdgsuctlem  10515  frecfzennn  10518  seq3f1olemstep  10606  expcl2lemap  10643  leexp1a  10686  expnbnd  10755  faclbnd  10833  faclbnd6  10836  facavg  10838  fihasheqf1oi  10879  fihashf1rn  10880  fihashss  10908  fiubm  10920  seq3coll  10934  wrdsymb0  10967  wrdlenge2n0  10970  resqrexlemdecn  11177  qabsor  11240  cau3lem  11279  xrmaxiflemab  11412  xrmaxadd  11426  climcn2  11474  sumeq2  11524  sumrbdclem  11542  summodclem3  11545  summodclem2a  11546  zsumdc  11549  fsumgcl  11551  fsum3  11552  isumss  11556  fsumadd  11571  fsum2dlemstep  11599  fisum0diag2  11612  fsummulc2  11613  modfsummodlemstep  11622  fsumabs  11630  fsumrelem  11636  fsumiun  11642  isumshft  11655  mertenslem2  11701  prodeq2  11722  prodrbdclem  11736  prodmodclem3  11740  prodmodclem2a  11741  zproddc  11744  fprodseq  11748  fprodmul  11756  fprodconst  11785  fprodap0  11786  fprod2dlemstep  11787  fprodrec  11794  fprodsplit1f  11799  fprodap0f  11801  fprodle  11805  sin02gt0  11929  efieq1re  11937  p1modz1  11959  dvdsleabs2  12011  4dvdseven  12082  bitsfzo  12119  gcdeq0  12144  rppwr  12195  uzwodc  12204  algfx  12220  eucalgcvga  12226  lcmmndc  12230  lcmeq0  12239  qredeq  12264  isprm3  12286  rpexp  12321  sqpweven  12343  2sqpwodd  12344  phicl2  12382  phibnd  12385  phiprmpw  12390  fermltl  12402  pythagtriplem4  12437  pythagtriplem6  12439  pythagtriplem7  12440  pythagtriplem12  12444  pythagtriplem13  12445  pythagtriplem14  12446  pythagtriplem16  12448  pcdvdsb  12489  pc2dvds  12499  difsqpwdvds  12507  pcmpt  12512  pcmptdvds  12514  fldivp1  12517  prmpwdvds  12524  infpnlem1  12528  1arith  12536  4sqlem11  12570  ennnfonelemk  12617  ennnfonelemhom  12632  ennnfonelemrnh  12633  ennnfonelemf1  12635  ctinf  12647  ctiunctlemudc  12654  ctiunctlemf  12655  nninfdclemp1  12667  strslfvd  12720  strslfv2d  12721  strslssd  12725  imasival  12949  imasbas  12950  imasplusg  12951  imasaddfnlemg  12957  imasaddvallemg  12958  qusaddvallemg  12976  qusaddflemg  12977  qusaddval  12978  qusaddf  12979  qusmulval  12980  qusmulf  12981  lidrididd  13025  gsumfzval  13034  sgrpidmndm  13061  gsumfzz  13127  qusgrp2  13243  mulgnegnn  13262  eqgen  13357  rinvmod  13439  gsumfzconst  13471  qusrng  13514  srgdilem  13525  ringdilem  13568  qusring2  13622  lssintclm  13940  gsumfzfsumlemm  14143  eltg3  14293  iuncld  14351  cnss2  14463  txcnp  14507  uptx  14510  xblm  14653  metss  14730  fsumcncntop  14803  rescncf  14817  dedekindeulemlu  14857  suplociccex  14861  dedekindicclemlu  14866  dedekindicc  14869  ivthdec  14880  limccnp2lem  14912  dvaddxx  14939  dvmulxx  14940  dvrecap  14949  reeff1olem  15007  perfectlem2  15236  lgsval  15245  lgsfvalg  15246  lgsfcl2  15247  lgscllem  15248  lgsval2lem  15251  lgsneg  15265  lgsdir2  15274  lgsdir  15276  lgsdi  15278  lgsne0  15279  lgsdirnn0  15288  lgsdinn0  15289  gausslemma2dlem0c  15292  m1lgs  15326  2lgslem1  15332  2lgs  15345  2lgsoddprm  15354  2sqlem6  15361  sumdc2  15445  pwle2  15643  subctctexmid  15645  nninfsellemeq  15658  exmidsbthrlem  15666  cndcap  15703