Metamath Proof Explorer


Theorem mul31

Description: Commutative/associative law. (Contributed by Scott Fenton, 3-Jan-2013)

Ref Expression
Assertion mul31 ABCABC=CBA

Proof

Step Hyp Ref Expression
1 mulcom BCBC=CB
2 1 oveq2d BCABC=ACB
3 2 3adant1 ABCABC=ACB
4 mulass ABCABC=ABC
5 mulcl CBCB
6 5 ancoms BCCB
7 6 3adant1 ABCCB
8 simp1 ABCA
9 7 8 mulcomd ABCCBA=ACB
10 3 4 9 3eqtr4d ABCABC=CBA