Metamath Proof Explorer

Theorem mul32

Description: Commutative/associative law. (Contributed by NM, 8-Oct-1999)

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

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 mulass ⊢ A ∈ ℂ ∧ C ∈ ℂ ∧ B ∈ ℂ → A ⁢ C ⁢ B = A ⁢ C ⁢ B
6 5 3com23 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A ⁢ C ⁢ B = A ⁢ C ⁢ B
7 3 4 6 3eqtr4d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A ⁢ B ⁢ C = A ⁢ C ⁢ B