This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$⊢ φ \to A \in ℂ$
	mul13d.2	$⊢ φ \to B \in ℂ$
	mul13d.3	$⊢ φ \to C \in ℂ$
Assertion	mul13d	$⊢ φ \to A B C = C B A$

Proof

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