Theorem mul13d

Description: Commutative/associative law that swaps the first and the third factor in a triple product. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	mul13d.1	$$⊢\phi \to A\in ℂ$$
	mul13d.2	$$⊢\phi \to B\in ℂ$$
	mul13d.3	$$⊢\phi \to C\in ℂ$$
Assertion	mul13d	$$⊢\phi \to ABC=CBA$$

Proof

Step	Hyp	Ref	Expression
1		mul13d.1	$$⊢\phi \to A\in ℂ$$
2		mul13d.2	$$⊢\phi \to B\in ℂ$$
3		mul13d.3	$$⊢\phi \to C\in ℂ$$
4	1 2 3	mul12d	$$⊢\phi \to ABC=BAC$$
5	2 1 3	mulassd	$$⊢\phi \to BAC=BAC$$
6	2 1	mulcld	$$⊢\phi \to BA\in ℂ$$
7	6 3	mulcomd	$$⊢\phi \to BAC=CBA$$
8	4 5 7	3eqtr2d	$$⊢\phi \to ABC=CBA$$