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

Metamath Proof Explorer

Theorem mul4r

Description: Rearrangement of 4 factors: swap the right factors in the factors of a product of two products. (Contributed by AV, 4-Mar-2023)

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

Proof

Step Hyp Ref Expression
1 mulcom ⊢ C ∈ ℂ ∧ D ∈ ℂ → C ⁢ D = D ⁢ C
2 1 adantl ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → C ⁢ D = D ⁢ C
3 2 oveq2d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → A ⁢ B ⁢ C ⁢ D = A ⁢ B ⁢ D ⁢ C
4 mul4 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ D ∈ ℂ ∧ C ∈ ℂ → A ⁢ B ⁢ D ⁢ C = A ⁢ D ⁢ B ⁢ C
5 4 ancom2s ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → A ⁢ B ⁢ D ⁢ C = A ⁢ D ⁢ B ⁢ C
6 simplr ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → B ∈ ℂ
7 simprl ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → C ∈ ℂ
8 6 7 mulcomd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → B ⁢ C = C ⁢ B
9 8 oveq2d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → A ⁢ D ⁢ B ⁢ C = A ⁢ D ⁢ C ⁢ B
10 3 5 9 3eqtrd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → A ⁢ B ⁢ C ⁢ D = A ⁢ D ⁢ C ⁢ B