Metamath Proof Explorer


Theorem prodeq1d

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 )

Proof

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 )