![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > srgmnd | Structured version Visualization version GIF version |
Description: A semiring is a monoid. (Contributed by Thierry Arnoux, 21-Mar-2018.) |
Ref | Expression |
---|---|
srgmnd | ⊢ (𝑅 ∈ SRing → 𝑅 ∈ Mnd) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | srgcmn 20094 | . 2 ⊢ (𝑅 ∈ SRing → 𝑅 ∈ CMnd) | |
2 | cmnmnd 19717 | . 2 ⊢ (𝑅 ∈ CMnd → 𝑅 ∈ Mnd) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝑅 ∈ SRing → 𝑅 ∈ Mnd) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2098 Mndcmnd 18667 CMndccmn 19700 SRingcsrg 20091 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2697 ax-nul 5299 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-sb 2060 df-clab 2704 df-cleq 2718 df-clel 2804 df-ne 2935 df-ral 3056 df-rex 3065 df-rab 3427 df-v 3470 df-sbc 3773 df-dif 3946 df-un 3948 df-in 3950 df-ss 3960 df-nul 4318 df-if 4524 df-sn 4624 df-pr 4626 df-op 4630 df-uni 4903 df-br 5142 df-iota 6489 df-fv 6545 df-ov 7408 df-cmn 19702 df-srg 20092 |
This theorem is referenced by: srg0cl 20105 srgacl 20110 srgcom4 20119 srg1zr 20120 srgmulgass 20122 srgpcomppsc 20125 srglmhm 20126 srgrmhm 20127 srgsummulcr 20128 sgsummulcl 20129 srgbinomlem2 20132 srgbinomlem3 20133 srgbinomlem4 20134 srgbinomlem 20135 srgbinom 20136 slmdacl 32860 slmdsn0 32862 |
Copyright terms: Public domain | W3C validator |