Metamath Proof Explorer

Theorem mul31

Description: Commutative/associative law. (Contributed by Scott Fenton, 3-Jan-2013)

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

Proof

Step Hyp Ref Expression
1 mulcom ⊢ B ∈ ℂ ∧ C ∈ ℂ → B ⁢ C = C ⁢ B
2 1 oveq2d ⊢ B ∈ ℂ ∧ C ∈ ℂ → A ⁢ B ⁢ C = A ⁢ C ⁢ B
3 2 3adant1 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A ⁢ B ⁢ C = A ⁢ C ⁢ B
4 mulass ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A ⁢ B ⁢ C = A ⁢ B ⁢ C
5 mulcl ⊢ C ∈ ℂ ∧ B ∈ ℂ → C ⁢ B ∈ ℂ
6 5 ancoms ⊢ B ∈ ℂ ∧ C ∈ ℂ → C ⁢ B ∈ ℂ
7 6 3adant1 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → C ⁢ B ∈ ℂ
8 simp1 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A ∈ ℂ
9 7 8 mulcomd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → C ⁢ B ⁢ A = A ⁢ C ⁢ B
10 3 4 9 3eqtr4d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A ⁢ B ⁢ C = C ⁢ B ⁢ A