Metamath Proof Explorer

Theorem srgmnd

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

Ref Expression
Assertion srgmnd 
|- ( R e. SRing -> R e. Mnd )

Proof

Step Hyp Ref Expression
1 srgcmn 
 |-  ( R e. SRing -> R e. CMnd )
2 cmnmnd 
 |-  ( R e. CMnd -> R e. Mnd )
3 1 2 syl 
 |-  ( R e. SRing -> R e. Mnd )