Metamath Proof Explorer


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 )