Theorem dmmcand

Description: Cancellation law for division and multiplication. (Contributed by Glauco Siliprandi, 5-Apr-2020)

	Ref	Expression
Hypotheses	dmmcand.a	$$⊢\phi \to A\in ℂ$$
	dmmcand.b	$$⊢\phi \to B\in ℂ$$
	dmmcand.c	$$⊢\phi \to C\in ℂ$$
	dmmcand.bn0	$$⊢\phi \to B\ne 0$$
Assertion	dmmcand	$$⊢\phi \to \left(\frac{A}{B}\right)BC=AC$$

Proof

Step	Hyp	Ref	Expression
1		dmmcand.a	$$⊢\phi \to A\in ℂ$$
2		dmmcand.b	$$⊢\phi \to B\in ℂ$$
3		dmmcand.c	$$⊢\phi \to C\in ℂ$$
4		dmmcand.bn0	$$⊢\phi \to B\ne 0$$
5	2 3	mulcld	$$⊢\phi \to BC\in ℂ$$
6	1 2 5 4	div32d	$$⊢\phi \to \left(\frac{A}{B}\right)BC=A\left(\frac{BC}{B}\right)$$
7	3 2 4	divcan3d	$$⊢\phi \to \frac{BC}{B}=C$$
8	7	oveq2d	$$⊢\phi \to A\left(\frac{BC}{B}\right)=AC$$
9		eqidd	$$⊢\phi \to AC=AC$$
10	6 8 9	3eqtrd	$$⊢\phi \to \left(\frac{A}{B}\right)BC=AC$$