Description: A commutative ring's multiplication operation is commutative. (Contributed by Mario Carneiro, 7-Jan-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | ringcl.b | |
|
ringcl.t | |
||
Assertion | crngcom | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ringcl.b | |
|
2 | ringcl.t | |
|
3 | eqid | |
|
4 | 3 | crngmgp | |
5 | 3 1 | mgpbas | |
6 | 3 2 | mgpplusg | |
7 | 5 6 | cmncom | |
8 | 4 7 | syl3an1 | |