Metamath Proof Explorer


Theorem crngmgp

Description: A commutative ring's multiplication operation is commutative. (Contributed by Mario Carneiro, 7-Jan-2015)

Ref Expression
Hypothesis ringmgp.g G=mulGrpR
Assertion crngmgp RCRingGCMnd

Proof

Step Hyp Ref Expression
1 ringmgp.g G=mulGrpR
2 1 iscrng RCRingRRingGCMnd
3 2 simprbi RCRingGCMnd