Metamath Proof Explorer


Theorem mulcan2

Description: Cancellation law for multiplication. (Contributed by NM, 21-Jan-2005) (Revised by Mario Carneiro, 27-May-2016)

Ref Expression
Assertion mulcan2 A B C C 0 A C = B C A = B

Proof

Step Hyp Ref Expression
1 simp1 A B C C 0 A
2 simp2 A B C C 0 B
3 simp3l A B C C 0 C
4 simp3r A B C C 0 C 0
5 1 2 3 4 mulcan2d A B C C 0 A C = B C A = B