Metamath Proof Explorer


Theorem sumeq2d

Description: Equality deduction for sum. Note that unlike sumeq2dv , k may occur in ph . (Contributed by NM, 1-Nov-2005)

Ref Expression
Hypothesis sumeq2d.1 φ k A B = C
Assertion sumeq2d φ k A B = k A C

Proof

Step Hyp Ref Expression
1 sumeq2d.1 φ k A B = C
2 sumeq2 k A B = C k A B = k A C
3 1 2 syl φ k A B = k A C