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

Metamath Proof Explorer

Theorem mul4d

Description: Rearrangement of 4 factors. (Contributed by Mario Carneiro, 27-May-2016)

Ref Expression
Hypotheses muld.1 ⊢ φ → A ∈ ℂ
addcomd.2 ⊢ φ → B ∈ ℂ
addcand.3 ⊢ φ → C ∈ ℂ
mul4d.4 ⊢ φ → D ∈ ℂ
Assertion mul4d ⊢ φ → A ⁢ B ⁢ C ⁢ D = A ⁢ C ⁢ B ⁢ D

Proof

Step Hyp Ref Expression
1 muld.1 ⊢ φ → A ∈ ℂ
2 addcomd.2 ⊢ φ → B ∈ ℂ
3 addcand.3 ⊢ φ → C ∈ ℂ
4 mul4d.4 ⊢ φ → D ∈ ℂ
5 mul4 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → A ⁢ B ⁢ C ⁢ D = A ⁢ C ⁢ B ⁢ D
6 1 2 3 4 5 syl22anc ⊢ φ → A ⁢ B ⁢ C ⁢ D = A ⁢ C ⁢ B ⁢ D