Theorem mvllmuld

Description: Move LHS left multiplication to RHS. (Contributed by David A. Wheeler, 15-Oct-2018)

	Ref	Expression
Hypotheses	mvllmuld.1	$$⊢\phi \to A\in ℂ$$
	mvllmuld.2	$$⊢\phi \to B\in ℂ$$
	mvllmuld.3	$$⊢\phi \to A\ne 0$$
	mvllmuld.4	$$⊢\phi \to AB=C$$
Assertion	mvllmuld	$$⊢\phi \to B=\frac{C}{A}$$

Proof

Step	Hyp	Ref	Expression
1		mvllmuld.1	$$⊢\phi \to A\in ℂ$$
2		mvllmuld.2	$$⊢\phi \to B\in ℂ$$
3		mvllmuld.3	$$⊢\phi \to A\ne 0$$
4		mvllmuld.4	$$⊢\phi \to AB=C$$
5	2 1 3	divcan4d	$$⊢\phi \to \frac{BA}{A}=B$$
6	1 2	mulcomd	$$⊢\phi \to AB=BA$$
7	6 4	eqtr3d	$$⊢\phi \to BA=C$$
8	7	oveq1d	$$⊢\phi \to \frac{BA}{A}=\frac{C}{A}$$
9	5 8	eqtr3d	$$⊢\phi \to B=\frac{C}{A}$$