Theorem srgmnd 20217

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

Syntax hints:   → wi 4   ∈ wcel 2108  Mndcmnd 18772  CMndccmn 19822  SRingcsrg 20213

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-nul 5324

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ne 2947  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-sbc 3805  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-iota 6525  df-fv 6581  df-ov 7451  df-cmn 19824  df-srg 20214

This theorem is referenced by:  srg0cl  20227  srgacl  20232  srgcom4  20241  srg1zr  20242  srgmulgass  20244  srgpcomppsc  20247  srglmhm  20248  srgrmhm  20249  srgsummulcr  20250  sgsummulcl  20251  srgbinomlem2  20254  srgbinomlem3  20255  srgbinomlem4  20256  srgbinomlem  20257  srgbinom  20258  slmdacl  33188  slmdsn0  33190