Theorem ringcmn

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

	Ref	Expression
Assertion	ringcmn	$$⊢R\in \mathrm{Ring}\to R\in \mathrm{CMnd}$$

Proof

Step	Hyp	Ref	Expression
1		ringabl	$$⊢R\in \mathrm{Ring}\to R\in \mathrm{Abel}$$
2		ablcmn	$$⊢R\in \mathrm{Abel}\to R\in \mathrm{CMnd}$$
3	1 2	syl	$$⊢R\in \mathrm{Ring}\to R\in \mathrm{CMnd}$$