Metamath Proof Explorer


Theorem mul12d

Description: Commutative/associative law that swaps the first 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 mul12d φABC=BAC

Proof

Step Hyp Ref Expression
1 muld.1 φA
2 addcomd.2 φB
3 addcand.3 φC
4 mul12 ABCABC=BAC
5 1 2 3 4 syl3anc φABC=BAC