Metamath Proof Explorer


Theorem mpteq1OLD

Description: Obsolete version of mpteq1 as of 11-Nov-2024. (Contributed by Mario Carneiro, 16-Dec-2013) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion mpteq1OLD A=BxAC=xBC

Proof

Step Hyp Ref Expression
1 eqidd xAC=C
2 1 rgen xAC=C
3 mpteq12 A=BxAC=CxAC=xBC
4 2 3 mpan2 A=BxAC=xBC