Metamath Proof Explorer


Theorem dmdcand

Description: Cancellation law for division and multiplication. (Contributed by Mario Carneiro, 27-May-2016)

Ref Expression
Hypotheses div1d.1 φA
divcld.2 φB
divmuld.3 φC
divmuld.4 φB0
divdiv23d.5 φC0
Assertion dmdcand φBCAB=AC

Proof

Step Hyp Ref Expression
1 div1d.1 φA
2 divcld.2 φB
3 divmuld.3 φC
4 divmuld.4 φB0
5 divdiv23d.5 φC0
6 dmdcan BB0CC0ABCAB=AC
7 2 4 3 5 1 6 syl221anc φBCAB=AC