Theorem sumeq12sdv

Description: Equality deduction for sum. General version of sumeq2sdv . (Contributed by GG, 1-Sep-2025)

	Ref	Expression
Hypotheses	sumeq12sdv.1	|- ( ph -> A = B )
	sumeq12sdv.2	|- ( ph -> C = D )
Assertion	sumeq12sdv	|- ( ph -> sum_ k e. A C = sum_ k e. B D )

Proof

Step	Hyp	Ref	Expression
1		sumeq12sdv.1	|- ( ph -> A = B )
2		sumeq12sdv.2	|- ( ph -> C = D )
3	1	sumeq1d	|- ( ph -> sum_ k e. A C = sum_ k e. B C )
4	2	sumeq2sdv	|- ( ph -> sum_ k e. B C = sum_ k e. B D )
5	3 4	eqtrd	|- ( ph -> sum_ k e. A C = sum_ k e. B D )