Theorem sumeq12dv

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

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

Proof

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