Description: A commutative ring's multiplication operation is commutative. (Contributed by Mario Carneiro, 7-Jan-2015)
Ref | Expression | ||
---|---|---|---|
Hypothesis | ringmgp.g | |
|
Assertion | crngmgp | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ringmgp.g | |
|
2 | 1 | iscrng | |
3 | 2 | simprbi | |