mul12

Description: Commutative/associative law for multiplication. (Contributed by NM, 30-Apr-2005)

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

Step	Hyp	Ref	Expression
1		mulcom	$⊢ (A \in ℂ \land B \in ℂ) \to A B = B A$
2	1	oveq1d	$⊢ (A \in ℂ \land B \in ℂ) \to A B C = B A C$
3	2	3adant3	$⊢ (A \in ℂ \land B \in ℂ \land C \in ℂ) \to A B C = B A C$
4		mulass	$⊢ (A \in ℂ \land B \in ℂ \land C \in ℂ) \to A B C = A B C$
5		mulass	$⊢ (B \in ℂ \land A \in ℂ \land C \in ℂ) \to B A C = B A C$
6	5	3com12	$⊢ (A \in ℂ \land B \in ℂ \land C \in ℂ) \to B A C = B A C$
7	3 4 6	3eqtr3d	$⊢ (A \in ℂ \land B \in ℂ \land C \in ℂ) \to A B C = B A C$

Metamath Proof Explorer