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

Metamath Proof Explorer

Theorem mul4

Description: Rearrangement of 4 factors. (Contributed by NM, 8-Oct-1999)

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

Proof

Step Hyp Ref Expression
1 mul32 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A ⁢ B ⁢ C = A ⁢ C ⁢ B
2 1 oveq1d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A ⁢ B ⁢ C ⁢ D = A ⁢ C ⁢ B ⁢ D
3 2 3expa ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A ⁢ B ⁢ C ⁢ D = A ⁢ C ⁢ B ⁢ D
4 3 adantrr ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → A ⁢ B ⁢ C ⁢ D = A ⁢ C ⁢ B ⁢ D
5 mulcl ⊢ A ∈ ℂ ∧ B ∈ ℂ → A ⁢ B ∈ ℂ
6 mulass ⊢ A ⁢ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → A ⁢ B ⁢ C ⁢ D = A ⁢ B ⁢ C ⁢ D
7 6 3expb ⊢ A ⁢ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → A ⁢ B ⁢ C ⁢ D = A ⁢ B ⁢ C ⁢ D
8 5 7 sylan ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → A ⁢ B ⁢ C ⁢ D = A ⁢ B ⁢ C ⁢ D
9 mulcl ⊢ A ∈ ℂ ∧ C ∈ ℂ → A ⁢ C ∈ ℂ
10 mulass ⊢ A ⁢ C ∈ ℂ ∧ B ∈ ℂ ∧ D ∈ ℂ → A ⁢ C ⁢ B ⁢ D = A ⁢ C ⁢ B ⁢ D
11 10 3expb ⊢ A ⁢ C ∈ ℂ ∧ B ∈ ℂ ∧ D ∈ ℂ → A ⁢ C ⁢ B ⁢ D = A ⁢ C ⁢ B ⁢ D
12 9 11 sylan ⊢ A ∈ ℂ ∧ C ∈ ℂ ∧ B ∈ ℂ ∧ D ∈ ℂ → A ⁢ C ⁢ B ⁢ D = A ⁢ C ⁢ B ⁢ D
13 12 an4s ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → A ⁢ C ⁢ B ⁢ D = A ⁢ C ⁢ B ⁢ D
14 4 8 13 3eqtr3d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → A ⁢ B ⁢ C ⁢ D = A ⁢ C ⁢ B ⁢ D