Metamath Proof Explorer


Theorem ringcmn

Description: A ring is a commutative monoid. (Contributed by Mario Carneiro, 7-Jan-2015)

Ref Expression
Assertion ringcmn RRingRCMnd

Proof

Step Hyp Ref Expression
1 ringabl RRingRAbel
2 ablcmn RAbelRCMnd
3 1 2 syl RRingRCMnd