Theorem srgmnd 20227

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

Assertion

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

Proof of Theorem srgmnd

Step	Hyp	Ref	Expression
1		srgcmn 20226	. 2 ⊢ (𝑅 ∈ SRing → 𝑅 ∈ CMnd)
2		cmnmnd 19828	. 2 ⊢ (𝑅 ∈ CMnd → 𝑅 ∈ Mnd)
3	1, 2	syl 17	1 ⊢ (𝑅 ∈ SRing → 𝑅 ∈ Mnd)

Syntax hints:   → wi 4   ∈ wcel 2141  Mndcmnd 18759  CMndccmn 19811  SRingcsrg 20223

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-nul 5253

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-sbc 3743  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-if 4478  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-br 5098  df-iota 6472  df-fv 6524  df-ov 7394  df-cmn 19813  df-srg 20224

This theorem is referenced by:  srg0cl  20237  srgacl  20242  srgcom4  20251  srg1zr  20252  srgmulgass  20254  srgpcomppsc  20257  srglmhm  20258  srgrmhm  20259  srgsummulcr  20260  sgsummulcl  20261  srgbinomlem2  20264  srgbinomlem3  20265  srgbinomlem4  20266  srgbinomlem  20267  srgbinom  20268  slmdacl  33350  slmdsn0  33352