Metamath Proof Explorer


Theorem mvlrmuli

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

Ref Expression
Hypotheses mvlrmuli.1 A
mvlrmuli.2 B
mvlrmuli.3 B 0
mvlrmuli.4 A B = C
Assertion mvlrmuli A = C B

Proof

Step Hyp Ref Expression
1 mvlrmuli.1 A
2 mvlrmuli.2 B
3 mvlrmuli.3 B 0
4 mvlrmuli.4 A B = C
5 1 2 3 divcan4i A B B = A
6 4 oveq1i A B B = C B
7 5 6 eqtr3i A = C B