Metamath Proof Explorer


Theorem sumeq12rdv

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

Ref Expression
Hypotheses sumeq12rdv.1 ( 𝜑𝐴 = 𝐵 )
sumeq12rdv.2 ( ( 𝜑𝑘𝐵 ) → 𝐶 = 𝐷 )
Assertion sumeq12rdv ( 𝜑 → Σ 𝑘𝐴 𝐶 = Σ 𝑘𝐵 𝐷 )

Proof

Step Hyp Ref Expression
1 sumeq12rdv.1 ( 𝜑𝐴 = 𝐵 )
2 sumeq12rdv.2 ( ( 𝜑𝑘𝐵 ) → 𝐶 = 𝐷 )
3 1 sumeq1d ( 𝜑 → Σ 𝑘𝐴 𝐶 = Σ 𝑘𝐵 𝐶 )
4 2 sumeq2dv ( 𝜑 → Σ 𝑘𝐵 𝐶 = Σ 𝑘𝐵 𝐷 )
5 3 4 eqtrd ( 𝜑 → Σ 𝑘𝐴 𝐶 = Σ 𝑘𝐵 𝐷 )