Theorem srgmnd 20103

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 20102	. 2 ⊢ (𝑅 ∈ SRing → 𝑅 ∈ CMnd)
2		cmnmnd 19704	. 2 ⊢ (𝑅 ∈ CMnd → 𝑅 ∈ Mnd)
3	1, 2	syl 17	1 ⊢ (𝑅 ∈ SRing → 𝑅 ∈ Mnd)

Syntax hints:   → wi 4   ∈ wcel 2111  Mndcmnd 18637  CMndccmn 19687  SRingcsrg 20099

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-nul 5239

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ne 2929  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-sbc 3737  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4279  df-if 4471  df-sn 4572  df-pr 4574  df-op 4578  df-uni 4855  df-br 5087  df-iota 6432  df-fv 6484  df-ov 7344  df-cmn 19689  df-srg 20100

This theorem is referenced by:  srg0cl  20113  srgacl  20118  srgcom4  20127  srg1zr  20128  srgmulgass  20130  srgpcomppsc  20133  srglmhm  20134  srgrmhm  20135  srgsummulcr  20136  sgsummulcl  20137  srgbinomlem2  20140  srgbinomlem3  20141  srgbinomlem4  20142  srgbinomlem  20143  srgbinom  20144  slmdacl  33170  slmdsn0  33172