Theorem ringcmn

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

	Ref	Expression
Assertion	ringcmn	⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ CMnd )

Proof

Step	Hyp	Ref	Expression
1		ringabl	⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Abel )
2		ablcmn	⊢ ( 𝑅 ∈ Abel → 𝑅 ∈ CMnd )
3	1 2	syl	⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ CMnd )