Description: Equality deduction for sum. (Contributed by NM, 1-Dec-2005)
Ref | Expression | ||
---|---|---|---|
Hypotheses | sumeq12dv.1 | |
|
sumeq12dv.2 | |
||
Assertion | sumeq12dv | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sumeq12dv.1 | |
|
2 | sumeq12dv.2 | |
|
3 | 2 | sumeq2dv | |
4 | 1 | sumeq1d | |
5 | 3 4 | eqtrd | |