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 ) |
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 ) |