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	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
	mul13d.2	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
	mul13d.3	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
Assertion	mul13d	⊢ ( 𝜑 → ( 𝐴 · ( 𝐵 · 𝐶 ) ) = ( 𝐶 · ( 𝐵 · 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		mul13d.1	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
2		mul13d.2	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
3		mul13d.3	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
4	1 2 3	mul12d	⊢ ( 𝜑 → ( 𝐴 · ( 𝐵 · 𝐶 ) ) = ( 𝐵 · ( 𝐴 · 𝐶 ) ) )
5	2 1 3	mulassd	⊢ ( 𝜑 → ( ( 𝐵 · 𝐴 ) · 𝐶 ) = ( 𝐵 · ( 𝐴 · 𝐶 ) ) )
6	2 1	mulcld	⊢ ( 𝜑 → ( 𝐵 · 𝐴 ) ∈ ℂ )
7	6 3	mulcomd	⊢ ( 𝜑 → ( ( 𝐵 · 𝐴 ) · 𝐶 ) = ( 𝐶 · ( 𝐵 · 𝐴 ) ) )
8	4 5 7	3eqtr2d	⊢ ( 𝜑 → ( 𝐴 · ( 𝐵 · 𝐶 ) ) = ( 𝐶 · ( 𝐵 · 𝐴 ) ) )