Theorem sumeq1i 13520

Description: Equality inference for sum. (Contributed by NM, 2-Jan-2006.)

Hypothesis

Ref	Expression
sumeq1i.1

Assertion

Ref	Expression
sumeq1i

Distinct variable groups:   ,   ,

Proof of Theorem sumeq1i

Step	Hyp	Ref	Expression
1		sumeq1i.1	. 2
2		sumeq1 13511	. 2
3	1, 2	ax-mp 5	1

Syntax hints:  =wceq 1395  sum_csu 13508

This theorem is referenced by:  sumeq12i  13522  fsump1i  13584  fsum2d  13586  fsumxp  13587  isumnn0nn  13654  arisum  13671  arisum2  13672  geo2sum  13682  efsep  13845  ef4p  13848  rpnnen2  13959  ovolicc2lem4  21931  itg10  22095  dveflem  22380  dvply1  22680  vieta1lem2  22707  aaliou3lem4  22742  dvtaylp  22765  pserdvlem2  22823  advlogexp  23036  log2ublem2  23278  log2ublem3  23279  log2ub  23280  ftalem5  23350  cht1  23439  1sgmprm  23474  lgsquadlem2  23630  axlowdimlem16  24260  rusgranumwlks  24956  signsvf0  28537  signsvf1  28538  bpoly0  29812  bpoly1  29813  bpoly2  29819  bpoly3  29820  bpoly4  29821  binomcxplemnotnn0  31261  dvnmul  31740  stoweidlem17  31799  dirkertrigeqlem1  31880  etransclem24  32041  etransclem35  32052

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