Theorem esumeq12d

Description: Equality deduction for extended sum. (Contributed by Thierry Arnoux, 18-Feb-2017)

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

Proof

Step	Hyp	Ref	Expression
1		esumeq12d.1	|- ( ph -> A = B )
2		esumeq12d.2	|- ( ph -> C = D )
3	2	adantr	|- ( ( ph /\ k e. A ) -> C = D )
4	1 3	esumeq12dva	|- ( ph -> sum* k e. A C = sum* k e. B D )