Theorem srgmnd

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

	Ref	Expression
Assertion	srgmnd	⊢ ( 𝑅 ∈ SRing → 𝑅 ∈ Mnd )

Proof

Step	Hyp	Ref	Expression
1		srgcmn	⊢ ( 𝑅 ∈ SRing → 𝑅 ∈ CMnd )
2		cmnmnd	⊢ ( 𝑅 ∈ CMnd → 𝑅 ∈ Mnd )
3	1 2	syl	⊢ ( 𝑅 ∈ SRing → 𝑅 ∈ Mnd )