mul32

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

Step	Hyp	Ref	Expression
1		mulcom	$⊢ (B \in ℂ \land C \in ℂ) \to B C = C B$
2	1	oveq2d	$⊢ (B \in ℂ \land C \in ℂ) \to A B C = A C B$
3	2	3adant1	$⊢ (A \in ℂ \land B \in ℂ \land C \in ℂ) \to A B C = A C B$
4		mulass	$⊢ (A \in ℂ \land B \in ℂ \land C \in ℂ) \to A B C = A B C$
5		mulass	$⊢ (A \in ℂ \land C \in ℂ \land B \in ℂ) \to A C B = A C B$
6	5	3com23	$⊢ (A \in ℂ \land B \in ℂ \land C \in ℂ) \to A C B = A C B$
7	3 4 6	3eqtr4d	$⊢ (A \in ℂ \land B \in ℂ \land C \in ℂ) \to A B C = A C B$

Metamath Proof Explorer