Metamath Proof Explorer


Theorem prodeq2i

Description: Equality inference for product. (Contributed by Scott Fenton, 4-Dec-2017)

Ref Expression
Hypothesis prodeq2i.1 kAB=C
Assertion prodeq2i kAB=kAC

Proof

Step Hyp Ref Expression
1 prodeq2i.1 kAB=C
2 prodeq2 kAB=CkAB=kAC
3 2 1 mprg kAB=kAC