Theorem srgmnd 18863

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

Syntax hints:   → wi 4   ∈ wcel 2166  Mndcmnd 17647  CMndccmn 18546  SRingcsrg 18859

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2391  ax-ext 2803  ax-nul 5013

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3an 1115  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-mo 2605  df-eu 2640  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ral 3122  df-rex 3123  df-rab 3126  df-v 3416  df-sbc 3663  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-nul 4145  df-if 4307  df-sn 4398  df-pr 4400  df-op 4404  df-uni 4659  df-br 4874  df-iota 6086  df-fv 6131  df-ov 6908  df-cmn 18548  df-srg 18860

This theorem is referenced by:  srg0cl  18873  srgacl  18878  srg1zr  18883  srgmulgass  18885  srgpcomppsc  18888  srglmhm  18889  srgrmhm  18890  srgsummulcr  18891  sgsummulcl  18892  srgbinomlem2  18895  srgbinomlem3  18896  srgbinomlem4  18897  srgbinomlem  18898  srgbinom  18899  slmdacl  30307  slmdsn0  30309