Theorem mvlrmuld

Description: Move the right term in a product on the LHS to the RHS, deduction form. (Contributed by David A. Wheeler, 11-Oct-2018)

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

Proof

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