Theorem ringmnd

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

	Ref	Expression
Assertion	ringmnd	$$⊢R\in \mathrm{Ring}\to R\in \mathrm{Mnd}$$

Proof

Step	Hyp	Ref	Expression
1		ringgrp	$$⊢R\in \mathrm{Ring}\to R\in \mathrm{Grp}$$
2	1	grpmndd	$$⊢R\in \mathrm{Ring}\to R\in \mathrm{Mnd}$$