Metamath Proof Explorer

Theorem mul12

Description: Commutative/associative law for multiplication. (Contributed by NM, 30-Apr-2005)

Ref Expression
Assertion mul12 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A ⁢ B ⁢ C = B ⁢ A ⁢ C

Proof

Step Hyp Ref Expression
1 mulcom ⊢ A ∈ ℂ ∧ B ∈ ℂ → A ⁢ B = B ⁢ A
2 1 oveq1d ⊢ A ∈ ℂ ∧ B ∈ ℂ → A ⁢ B ⁢ C = B ⁢ A ⁢ C
3 2 3adant3 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A ⁢ B ⁢ C = B ⁢ A ⁢ C
4 mulass ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A ⁢ B ⁢ C = A ⁢ B ⁢ C
5 mulass ⊢ B ∈ ℂ ∧ A ∈ ℂ ∧ C ∈ ℂ → B ⁢ A ⁢ C = B ⁢ A ⁢ C
6 5 3com12 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → B ⁢ A ⁢ C = B ⁢ A ⁢ C
7 3 4 6 3eqtr3d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A ⁢ B ⁢ C = B ⁢ A ⁢ C