MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sumeq1d Unicode version

Theorem sumeq1d 12190
Description: Equality deduction for sum. (Contributed by NM, 1-Nov-2005.)
Hypothesis
Ref Expression
sumeq1d.1  |-  ( ph  ->  A  =  B )
Assertion
Ref Expression
sumeq1d  |-  ( ph  -> 
sum_ k  e.  A  C  =  sum_ k  e.  B  C )
Distinct variable groups:    A, k    B, k
Allowed substitution hints:    ph( k)    C( k)

Proof of Theorem sumeq1d
StepHypRef Expression
1 sumeq1d.1 . 2  |-  ( ph  ->  A  =  B )
2 sumeq1 12178 . 2  |-  ( A  =  B  ->  sum_ k  e.  A  C  =  sum_ k  e.  B  C
)
31, 2syl 15 1  |-  ( ph  -> 
sum_ k  e.  A  C  =  sum_ k  e.  B  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632   sum_csu 12174
This theorem is referenced by:  sumeq12dv  12195  sumeq12rdv  12196  fsumf1o  12212  sumss  12213  fsumcllem  12221  fsum1  12230  fzosump1  12233  fsump1  12235  fsum2d  12250  fsumcom2  12253  fsumshftm  12259  fsumrev2  12260  fsumtscopo  12276  fsumtscop  12278  fsumtscop2  12279  fsumparts  12280  fsumiun  12295  bcxmas  12310  incexclem  12311  incexc2  12313  isumsplit  12315  isum1p  12316  arisum  12334  arisum2  12335  geoser  12341  geolim  12342  geo2sum2  12346  mertenslem1  12356  mertenslem2  12357  mertens  12358  efcvgfsum  12383  eftlub  12405  effsumlt  12407  eirrlem  12498  bitsinv1  12649  bitsinvp1  12656  pcfac  12963  prmreclem4  12982  prmreclem6  12984  ovoliunlem1  18877  uniioombllem3  18956  itg11  19062  dvfsumlem1  19389  dvfsumlem4  19392  dvfsum2  19397  elplyr  19599  coeeu  19623  coeeq  19625  plyco  19639  0dgrb  19644  dvply2g  19681  vieta1lem2  19707  vieta1  19708  aaliou3lem5  19743  aaliou3lem6  19744  aaliou3lem7  19745  taylpfval  19760  pserdvlem2  19820  abelthlem6  19828  logfac  19970  advlogexp  20018  emcllem2  20306  emcllem3  20307  emcllem7  20311  harmonicbnd  20313  harmonicbnd2  20314  harmonicbnd3  20317  harmonicbnd4  20320  chtval  20364  chpval  20376  chtfl  20403  chpfl  20404  chtprm  20407  chtnprm  20408  chpp1  20409  chtdif  20412  prmorcht  20432  musum  20447  muinv  20449  logfaclbnd  20477  logfacbnd3  20478  logexprlim  20480  chtppilimlem1  20638  rplogsumlem2  20650  rpvmasumlem  20652  dchrisumlem1  20654  dchrisumlem2  20655  dchrisumlem3  20656  dchrisum  20657  dchrisum0fval  20670  dchrisum0ff  20672  dchrisum0flblem1  20673  dchrisum0lem2  20683  dchrisum0  20685  mulog2sumlem1  20699  2vmadivsumlem  20705  log2sumbnd  20709  logdivbnd  20721  selberg3lem1  20722  pntrsumbnd  20731  pntrsumbnd2  20732  pntrlog2bndlem1  20742  pntrlog2bndlem4  20745  pntpbnd1  20751  pntpbnd2  20752  pntlemf  20770  subfacval2  23733  subfaclim  23734  brcgr  24600  axlowdimlem16  24657  bpolydiflem  24861  mettrifi  26576  rrncmslem  26659  stoweidlem17  27869  stoweidlem20  27872  stirlinglem12  27937
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ral 2561  df-rex 2562  df-rab 2565  df-v 2803  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662  df-uni 3844  df-br 4040  df-opab 4094  df-mpt 4095  df-cnv 4713  df-dm 4715  df-rn 4716  df-res 4717  df-ima 4718  df-iota 5235  df-f 5275  df-f1 5276  df-fo 5277  df-f1o 5278  df-fv 5279  df-ov 5877  df-oprab 5878  df-mpt2 5879  df-recs 6404  df-rdg 6439  df-seq 11063  df-sum 12175
  Copyright terms: Public domain W3C validator