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		grpmnd	$$⊢R\in \mathrm{Grp}\to R\in \mathrm{Mnd}$$
3	1 2	syl	$$⊢R\in \mathrm{Ring}\to R\in \mathrm{Mnd}$$