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  2752  elex2  2753  spcimdv  2821  spcimedv  2823  spcedv  2826  rspcdva  2846  elabd  2882  spsbcd  2975  opth  4237  euotd  4254  ssorduni  4486  tfisi  4586  omsinds  4621  nnpredcl  4622  sotri2  5026  sotri3  5027  unielrel  5156  funmo  5231  fnfvima  5751  fliftfun  5796  fliftval  5800  riota5f  5854  riotass2  5856  oprssdmm  6171  tfrlem5  6314  tfrlemibxssdm  6327  tfrlemibfn  6328  tfrlemiex  6331  tfr1onlemsucfn  6340  tfr1onlemsucaccv  6341  tfr1onlembxssdm  6343  tfr1onlembfn  6344  tfr1onlemex  6347  tfr1onlemres  6349  tfrcllemsucfn  6353  tfrcllemsucaccv  6354  tfrcllembxssdm  6356  tfrcllembfn  6357  tfrcllemex  6360  tfrcllemres  6362  tfrcl  6364  rdgisucinc  6385  frecabex  6398  frecabcl  6399  nntr2  6503  ertr  6549  qliftlem  6612  th3q  6639  resixp  6732  f1dom2g  6755  dom3d  6773  en1  6798  xpdom3m  6833  xpf1o  6843  phplem4dom  6861  phpm  6864  phpelm  6865  findcard  6887  finexdc  6901  fiintim  6927  fisseneq  6930  ssfirab  6932  f1dmvrnfibi  6942  iunfidisj  6944  fidcenumlemrk  6952  dcfi  6979  suplub2ti  6999  supelti  7000  ordiso2  7033  caseinl  7089  caseinr  7090  djudom  7091  difinfsn  7098  difinfinf  7099  ctm  7107  enumct  7113  nnnninfeq  7125  ismkvnex  7152  exmidfodomrlemr  7200  exmidfodomrlemrALT  7201  acfun  7205  exmidontriimlem2  7220  exmidontriimlem3  7221  exmidapne  7258  cc2lem  7264  cc3  7266  recexnq  7388  ltbtwnnqq  7413  addnnnq0  7447  mulnnnq0  7448  prarloclemn  7497  prarloc  7501  distrlem1prl  7580  distrlem1pru  7581  distrlem4prl  7582  distrlem4pru  7583  ltexprlemrl  7608  cauappcvgprlemladdru  7654  cauappcvgprlemladdrl  7655  addsrpr  7743  mulsrpr  7744  map2psrprg  7803  axpre-suploclemres  7899  lemul12a  8818  lemulge11  8822  sup3exmid  8913  nngt0  8943  nn0ge0  9200  nn0ge2m1nn  9235  zletric  9296  zlelttric  9297  nn0n0n1ge2b  9331  nn0ind-raph  9369  supinfneg  9594  infsupneg  9595  infregelbex  9597  rpge0  9665  fz0fzelfz0  10126  fz0fzdiffz0  10129  ige2m2fzo  10197  elfzodifsumelfzo  10200  elfzom1elp1fzo  10201  exfzdc  10239  qletric  10243  qlelttric  10244  rebtwn2zlemshrink  10253  frecuzrdgtcl  10411  frecuzrdg0  10412  frecuzrdgfunlem  10418  frecuzrdg0t  10421  frecuzrdgsuctlem  10422  frecfzennn  10425  seq3f1olemstep  10500  expcl2lemap  10531  leexp1a  10574  expnbnd  10643  faclbnd  10720  faclbnd6  10723  facavg  10725  fihasheqf1oi  10766  fihashf1rn  10767  fihashss  10795  fiubm  10807  seq3coll  10821  resqrexlemdecn  11020  qabsor  11083  cau3lem  11122  xrmaxiflemab  11254  xrmaxadd  11268  climcn2  11316  sumeq2  11366  sumrbdclem  11384  summodclem3  11387  summodclem2a  11388  zsumdc  11391  fsumgcl  11393  fsum3  11394  isumss  11398  fsumadd  11413  fsum2dlemstep  11441  fisum0diag2  11454  fsummulc2  11455  modfsummodlemstep  11464  fsumabs  11472  fsumrelem  11478  fsumiun  11484  isumshft  11497  mertenslem2  11543  prodeq2  11564  prodrbdclem  11578  prodmodclem3  11582  prodmodclem2a  11583  zproddc  11586  fprodseq  11590  fprodmul  11598  fprodconst  11627  fprodap0  11628  fprod2dlemstep  11629  fprodrec  11636  fprodsplit1f  11641  fprodap0f  11643  fprodle  11647  sin02gt0  11770  efieq1re  11778  p1modz1  11800  dvdsleabs2  11851  4dvdseven  11921  gcdmndc  11944  zsupcllemstep  11945  infssuzex  11949  gcdsupex  11957  gcdsupcl  11958  gcdeq0  11977  gcdaddm  11984  rppwr  12028  uzwodc  12037  nnwosdc  12039  algfx  12051  eucalgcvga  12057  lcmmndc  12061  lcmval  12062  lcmcllem  12066  lcmledvds  12069  lcmeq0  12070  qredeq  12095  isprm3  12117  prmdc  12129  rpexp  12152  sqpweven  12174  2sqpwodd  12175  phicl2  12213  phibnd  12216  phiprmpw  12221  fermltl  12233  pythagtriplem4  12267  pythagtriplem6  12269  pythagtriplem7  12270  pythagtriplem12  12274  pythagtriplem13  12275  pythagtriplem14  12276  pythagtriplem16  12278  pclemdc  12287  pcdvdsb  12318  pc2dvds  12328  difsqpwdvds  12336  pcmpt  12340  pcmptdvds  12342  fldivp1  12345  prmpwdvds  12352  infpnlem1  12356  infpnlem2  12357  1arith  12364  ennnfonelemk  12400  ennnfonelemhom  12415  ennnfonelemrnh  12416  ennnfonelemf1  12418  ctinf  12430  ctiunctlemudc  12437  ctiunctlemf  12438  nninfdclemcl  12448  nninfdclemp1  12450  strslfvd  12503  strslfv2d  12504  strslssd  12508  imasival  12726  imasbas  12727  imasplusg  12728  imasaddfnlemg  12734  imasaddvallemg  12735  qusaddvallemg  12751  qusaddflemg  12752  qusaddval  12753  qusaddf  12754  qusmulval  12755  qusmulf  12756  lidrididd  12800  sgrpidmndm  12820  mulgnegnn  12992  eqgen  13084  rinvmod  13110  srgdilem  13150  ringdilem  13193  eltg3  13527  iuncld  13585  cnss2  13697  txcnp  13741  uptx  13744  xblm  13887  metss  13964  fsumcncntop  14026  rescncf  14038  dedekindeulemlu  14069  suplociccex  14073  dedekindicclemlu  14078  dedekindicc  14081  ivthdec  14092  limccnp2lem  14115  dvaddxx  14137  dvmulxx  14138  dvrecap  14147  reeff1olem  14162  lgsval  14375  lgsfvalg  14376  lgsfcl2  14377  lgscllem  14378  lgsval2lem  14381  lgsneg  14395  lgsdir2  14404  lgsdir  14406  lgsdi  14408  lgsne0  14409  lgsdirnn0  14418  lgsdinn0  14419  m1lgs  14422  2sqlem6  14437  sumdc2  14521  pwle2  14718  subctctexmid  14720  nninfsellemeq  14733  exmidsbthrlem  14740