Metamath Proof Explorer

Theorem srgmnd

Description: A semiring is a monoid. (Contributed by Thierry Arnoux, 21-Mar-2018)

		Ref	Expression
	Assertion	srgmnd	$⊢ R \in SRing \to R \in Mnd$

Step	Hyp	Ref	Expression
1		srgcmn	$⊢ R \in SRing \to R \in CMnd$
2		cmnmnd	$⊢ R \in CMnd \to R \in Mnd$
3	1 2	syl	$⊢ R \in SRing \to R \in Mnd$