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	|- ( ph -> A e. CC )
	mvlrmuld.2	|- ( ph -> B e. CC )
	mvlrmuld.3	|- ( ph -> B =/= 0 )
	mvlrmuld.4	|- ( ph -> ( A x. B ) = C )
Assertion	mvlrmuld	|- ( ph -> A = ( C / B ) )

Proof

Step	Hyp	Ref	Expression
1		mvlrmuld.1	|- ( ph -> A e. CC )
2		mvlrmuld.2	|- ( ph -> B e. CC )
3		mvlrmuld.3	|- ( ph -> B =/= 0 )
4		mvlrmuld.4	|- ( ph -> ( A x. B ) = C )
5	1 2 3	divcan4d	|- ( ph -> ( ( A x. B ) / B ) = A )
6	4	oveq1d	|- ( ph -> ( ( A x. B ) / B ) = ( C / B ) )
7	5 6	eqtr3d	|- ( ph -> A = ( C / B ) )