Metamath Proof Explorer


Theorem sumeq12dv

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

Ref Expression
Hypotheses sumeq12dv.1 φA=B
sumeq12dv.2 φkAC=D
Assertion sumeq12dv φkAC=kBD

Proof

Step Hyp Ref Expression
1 sumeq12dv.1 φA=B
2 sumeq12dv.2 φkAC=D
3 2 sumeq2dv φkAC=kAD
4 1 sumeq1d φkAD=kBD
5 3 4 eqtrd φkAC=kBD