Metamath Proof Explorer


Theorem divcan7d

Description: Cancel equal divisors in a division. (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 divcan7d φACBC=AB

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 divcan7 ABB0CC0ACBC=AB
7 1 2 4 3 5 6 syl122anc φACBC=AB