Theorem sumeq1d 13523

Description: Equality deduction for sum. (Contributed by NM, 1-Nov-2005.)

Hypothesis

Ref	Expression
sumeq1d.1

Assertion

Ref	Expression
sumeq1d

Distinct variable groups:   ,   ,

Proof of Theorem sumeq1d

Step	Hyp	Ref	Expression
1		sumeq1d.1	. 2
2		sumeq1 13511	. 2
3	1, 2	syl 16	1

Syntax hints:  ->wi 4  =wceq 1395  sum_csu 13508

This theorem is referenced by:  sumeq12dv  13528  sumeq12rdv  13529  fsumf1o  13545  sumss  13546  fsumcllem  13554  fsum1  13564  fzosump1  13567  fsump1  13571  fsum2d  13586  fsumcom2  13589  fsumshftm  13596  fsumrev2  13597  telfsumo  13616  telfsum  13618  telfsum2  13619  fsumparts  13620  fsumiun  13635  bcxmas  13647  incexclem  13648  incexc2  13650  isumsplit  13652  isum1p  13653  arisum  13671  arisum2  13672  geoser  13678  geolim  13679  geo2sum2  13683  mertenslem1  13693  mertenslem2  13694  mertens  13695  efcvgfsum  13821  fprodefsum  13830  eftlub  13844  effsumlt  13846  eirrlem  13937  bitsinv1  14092  bitsinvp1  14099  pcfac  14418  prmreclem4  14437  prmreclem6  14439  ovoliunlem1  21913  uniioombllem3  21994  itg11  22098  dvfsumlem1  22427  dvfsumlem4  22430  dvfsum2  22435  elplyr  22598  coeeu  22622  coeeq  22624  plyco  22638  0dgrb  22643  dvply2g  22681  vieta1lem2  22707  vieta1  22708  aaliou3lem5  22743  aaliou3lem6  22744  aaliou3lem7  22745  taylpfval  22760  pserdvlem2  22823  abelthlem6  22831  logfac  22985  advlogexp  23036  emcllem2  23326  emcllem3  23327  emcllem7  23331  harmonicbnd  23333  harmonicbnd2  23334  harmonicbnd3  23337  harmonicbnd4  23340  chtval  23384  chpval  23396  chtfl  23423  chpfl  23424  chtprm  23427  chtnprm  23428  chpp1  23429  chtdif  23432  prmorcht  23452  musum  23467  muinv  23469  logfaclbnd  23497  logfacbnd3  23498  logexprlim  23500  chtppilimlem1  23658  rplogsumlem2  23670  rpvmasumlem  23672  dchrisumlem1  23674  dchrisumlem2  23675  dchrisumlem3  23676  dchrisum  23677  dchrisum0fval  23690  dchrisum0ff  23692  dchrisum0flblem1  23693  dchrisum0lem2  23703  dchrisum0  23705  mulog2sumlem1  23719  2vmadivsumlem  23725  log2sumbnd  23729  logdivbnd  23741  selberg3lem1  23742  pntrsumbnd  23751  pntrsumbnd2  23752  pntrlog2bndlem1  23762  pntrlog2bndlem4  23765  pntpbnd1  23771  pntpbnd2  23772  pntlemf  23790  brcgr  24203  axlowdimlem16  24260  eengv  24282  eulerpartlemgs2  28319  signsvfn  28539  subfacval2  28631  subfaclim  28632  bpolydiflem  29816  mettrifi  30250  rrncmslem  30328  binomcxplemnn0  31254  fsumnncl  31572  fsumsplit1  31573  sumnnodd  31636  dvnmul  31740  dvnprodlem3  31745  itgspltprt  31778  stoweidlem17  31799  stoweidlem20  31802  stirlinglem12  31867  dirkertrigeqlem1  31880  dirkertrigeqlem3  31882  fourierdlem83  31972  fourierdlem112  32001  fourierdlem113  32002  elaa2lem  32016  etransclem32  32049  altgsumbcALT  32942

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-br 4453  df-opab 4511  df-mpt 4512  df-cnv 5012  df-dm 5014  df-rn 5015  df-res 5016  df-ima 5017  df-iota 5556  df-f 5597  df-f1 5598  df-fo 5599  df-f1o 5600  df-fv 5601  df-ov 6299  df-oprab 6300  df-mpt2 6301  df-recs 7061  df-rdg 7095  df-seq 12108  df-sum 13509