This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mvllmuld

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

Ref Expression
Hypotheses mvllmuld.1 ⊢ φ → A ∈ ℂ
mvllmuld.2 ⊢ φ → B ∈ ℂ
mvllmuld.3 ⊢ φ → A ≠ 0
mvllmuld.4 ⊢ φ → A ⁢ B = C
Assertion mvllmuld ⊢ φ → B = C A

Proof

Step Hyp Ref Expression
1 mvllmuld.1 ⊢ φ → A ∈ ℂ
2 mvllmuld.2 ⊢ φ → B ∈ ℂ
3 mvllmuld.3 ⊢ φ → A ≠ 0
4 mvllmuld.4 ⊢ φ → A ⁢ B = C
5 2 1 3 divcan4d ⊢ φ → B ⁢ A A = B
6 1 2 mulcomd ⊢ φ → A ⁢ B = B ⁢ A
7 6 4 eqtr3d ⊢ φ → B ⁢ A = C
8 7 oveq1d ⊢ φ → B ⁢ A A = C A
9 5 8 eqtr3d ⊢ φ → B = C A