Metamath Proof Explorer

Theorem mul32d

Description: Commutative/associative law that swaps the last two factors in a triple product. (Contributed by Mario Carneiro, 27-May-2016)

Ref Expression
Hypotheses muld.1 φ A
addcomd.2 φ B
addcand.3 φ C
Assertion mul32d φ A B C = A C B


Step Hyp Ref Expression
1 muld.1 φ A
2 addcomd.2 φ B
3 addcand.3 φ C
4 mul32 A B C A B C = A C B
5 1 2 3 4 syl3anc φ A B C = A C B