mul4

		Ref	Expression
	Assertion	mul4	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to A B C D = A C B D$

Step	Hyp	Ref	Expression
1		mul32	$⊢ (A \in ℂ \land B \in ℂ \land C \in ℂ) \to A B C = A C B$
2	1	oveq1d	$⊢ (A \in ℂ \land B \in ℂ \land C \in ℂ) \to A B C D = A C B D$
3	2	3expa	$⊢ ((A \in ℂ \land B \in ℂ) \land C \in ℂ) \to A B C D = A C B D$
4	3	adantrr	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to A B C D = A C B D$
5		mulcl	$⊢ (A \in ℂ \land B \in ℂ) \to A B \in ℂ$
6		mulass	$⊢ (A B \in ℂ \land C \in ℂ \land D \in ℂ) \to A B C D = A B C D$
7	6	3expb	$⊢ (A B \in ℂ \land (C \in ℂ \land D \in ℂ)) \to A B C D = A B C D$
8	5 7	sylan	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to A B C D = A B C D$
9		mulcl	$⊢ (A \in ℂ \land C \in ℂ) \to A C \in ℂ$
10		mulass	$⊢ (A C \in ℂ \land B \in ℂ \land D \in ℂ) \to A C B D = A C B D$
11	10	3expb	$⊢ (A C \in ℂ \land (B \in ℂ \land D \in ℂ)) \to A C B D = A C B D$
12	9 11	sylan	$⊢ ((A \in ℂ \land C \in ℂ) \land (B \in ℂ \land D \in ℂ)) \to A C B D = A C B D$
13	12	an4s	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to A C B D = A C B D$
14	4 8 13	3eqtr3d	$⊢ ((A \in ℂ \land B \in ℂ) \land (C \in ℂ \land D \in ℂ)) \to A B C D = A C B D$

Metamath Proof Explorer