Description: Equality deduction for product. (Contributed by Scott Fenton, 4-Dec-2017)
Ref | Expression | ||
---|---|---|---|
Hypothesis | prodeq1d.1 | |- ( ph -> A = B ) |
|
Assertion | prodeq1d | |- ( ph -> prod_ k e. A C = prod_ k e. B C ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | prodeq1d.1 | |- ( ph -> A = B ) |
|
2 | prodeq1 | |- ( A = B -> prod_ k e. A C = prod_ k e. B C ) |
|
3 | 1 2 | syl | |- ( ph -> prod_ k e. A C = prod_ k e. B C ) |