Theorem sumeq12rdv

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

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

Proof

Step	Hyp	Ref	Expression
1		sumeq12rdv.1	|- ( ph -> A = B )
2		sumeq12rdv.2	|- ( ( ph /\ k e. B ) -> C = D )
3	1	sumeq1d	|- ( ph -> sum_ k e. A C = sum_ k e. B C )
4	2	sumeq2dv	|- ( 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 )