Metamath Proof Explorer


Theorem dmdcan

Description: Cancellation law for division and multiplication. (Contributed by Scott Fenton, 7-Jun-2013) (Proof shortened by Fan Zheng, 3-Jul-2016)

Ref Expression
Assertion dmdcan AA0BB0CABCA=CB

Proof

Step Hyp Ref Expression
1 simp1l AA0BB0CA
2 simp3 AA0BB0CC
3 simp1r AA0BB0CA0
4 divcl CAA0CA
5 2 1 3 4 syl3anc AA0BB0CCA
6 simp2l AA0BB0CB
7 simp2r AA0BB0CB0
8 div23 ACABB0ACAB=ABCA
9 1 5 6 7 8 syl112anc AA0BB0CACAB=ABCA
10 divcan2 CAA0ACA=C
11 2 1 3 10 syl3anc AA0BB0CACA=C
12 11 oveq1d AA0BB0CACAB=CB
13 9 12 eqtr3d AA0BB0CABCA=CB