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