Theorem sumeq1d 6943

Description: Equality deduction for sum.

Hypothesis

Ref	Expression
sumeq1d.1	|- (ph -> A = B)

Assertion

Ref	Expression
sumeq1d	|- (ph -> sum_k e. A C = sum_k e. B C)

Proof of Theorem sumeq1d

Step	Hyp	Ref	Expression
1		sumeq1d.1	. 2 |- (ph -> A = B)
2		sumeq1 6935	. 2 |- (A = B -> sum_k e. A C = sum_k e. B C)
3	1, 2	syl 10	1 |- (ph -> sum_k e. A C = sum_k e. B C)

Syntax hints:   -> wi 3   = wceq 955  sum_csu 6932

This theorem is referenced by:  sumeq12dv 6948  sumeq12rdv 6949  fsum1slem 6961  fsump1slem 6965  fsumcllem 6967  fsum1ps 6971  fsumsplit 6973  fsumadd 6975  fsum3 6977  fsum4 6978  csbfsumlem 6979  fsumcom 6981  fsumrev 6982  fsumrev2 6983  fsummulc1 6986  fsumconst 6991  fsumcmp 6993  fsumcmpndx2 6995  fsumabs 6996  ser1ser0 7001  bcxmas 7029  fsum0diaglem2 7209  fsum0diag 7210  efaddlem24 7320  efaddlem26 7322  efaddlem27 7323  ef1tlub 7341  ef01tlub 7344  absef01tlub 7346  fsumcnlem 7951

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 961  ax-gen 962  ax-8 963  ax-10 965  ax-12 967  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122  ax-10o 1139  ax-16 1209  ax-11o 1217  ax-ext 1458

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 980  df-sb 1171  df-clab 1463  df-cleq 1468  df-clel 1471  df-rex 1648  df-v 1809  df-un 2047  df-uni 2500  df-sum 6933

Copyright terms: Public domain