Description: Equality inference for product. (Contributed by Scott Fenton, 4-Dec-2017)
Ref | Expression | ||
---|---|---|---|
Hypotheses | prodeq12i.1 | |- A = B |
|
prodeq12i.2 | |- ( k e. A -> C = D ) |
||
Assertion | prodeq12i | |- prod_ k e. A C = prod_ k e. B D |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | prodeq12i.1 | |- A = B |
|
2 | prodeq12i.2 | |- ( k e. A -> C = D ) |
|
3 | 2 | prodeq2i | |- prod_ k e. A C = prod_ k e. A D |
4 | 1 | prodeq1i | |- prod_ k e. A D = prod_ k e. B D |
5 | 3 4 | eqtri | |- prod_ k e. A C = prod_ k e. B D |