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

Metamath Proof Explorer

Theorem mul4i

Description: Rearrangement of 4 factors. (Contributed by NM, 16-Feb-1995)

Ref Expression
Hypotheses mul.1 ⊢ A ∈ ℂ
mul.2 ⊢ B ∈ ℂ
mul.3 ⊢ C ∈ ℂ
mul4.4 ⊢ D ∈ ℂ
Assertion mul4i ⊢ A ⁢ B ⁢ C ⁢ D = A ⁢ C ⁢ B ⁢ D

Proof

Step Hyp Ref Expression
1 mul.1 ⊢ A ∈ ℂ
2 mul.2 ⊢ B ∈ ℂ
3 mul.3 ⊢ C ∈ ℂ
4 mul4.4 ⊢ D ∈ ℂ
5 mul4 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → A ⁢ B ⁢ C ⁢ D = A ⁢ C ⁢ B ⁢ D
6 1 2 3 4 5 mp4an ⊢ A ⁢ B ⁢ C ⁢ D = A ⁢ C ⁢ B ⁢ D