| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > grpmndd | Structured version Visualization version GIF version | ||
| Description: A group is a monoid. (Contributed by SN, 1-Jun-2024.) |
| Ref | Expression |
|---|---|
| grpmndd.1 | ⊢ (𝜑 → 𝐺 ∈ Grp) |
| Ref | Expression |
|---|---|
| grpmndd | ⊢ (𝜑 → 𝐺 ∈ Mnd) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | grpmndd.1 | . 2 ⊢ (𝜑 → 𝐺 ∈ Grp) | |
| 2 | grpmnd 18874 | . 2 ⊢ (𝐺 ∈ Grp → 𝐺 ∈ Mnd) | |
| 3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → 𝐺 ∈ Mnd) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∈ wcel 2114 Mndcmnd 18663 Grpcgrp 18867 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-ext 2709 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-sb 2069 df-clab 2716 df-cleq 2729 df-clel 2812 df-ral 3053 df-rex 3062 df-rab 3401 df-v 3443 df-dif 3905 df-un 3907 df-ss 3919 df-nul 4287 df-if 4481 df-sn 4582 df-pr 4584 df-op 4588 df-uni 4865 df-br 5100 df-iota 6449 df-fv 6501 df-ov 7363 df-grp 18870 |
| This theorem is referenced by: grpmgmd 18895 hashfingrpnn 18906 xpsinv 18994 ghmgrp 19000 mulgdirlem 19039 ghmmhm 19159 gsumccatsymgsn 19359 symggen 19403 symgtrinv 19405 psgnunilem2 19428 psgneldm2 19437 psgnfitr 19450 lsmass 19602 frgpmhm 19698 frgpuplem 19705 frgpupf 19706 frgpup1 19708 isabld 19728 gsumzinv 19878 telgsumfzslem 19921 telgsumfzs 19922 dprdssv 19951 dprdfadd 19955 pgpfac1lem3a 20011 prdsrngd 20115 ringmnd 20182 unitabl 20324 unitsubm 20326 lmodvsmmulgdi 20852 rngqiprngimf1 21259 psgnghm 21539 psdmul 22113 psdmvr 22116 ply1chr 22254 rhmcomulmpl 22330 clmmulg 25061 dchrptlem3 27237 abliso 33099 gsummulgc2 33130 cyc3genpmlem 33214 elrgspnsubrunlem2 33311 gsumind 33407 quslsm 33467 evl1deg1 33638 evl1deg2 33639 evl1deg3 33640 vr1nz 33655 r1pquslmic 33673 mplmulmvr 33685 mplvrpmmhm 33692 lvecendof1f1o 33771 extdgfialglem1 33830 algextdeglem4 33858 algextdeglem5 33859 rtelextdg2lem 33864 aks6d1c6lem5 42468 rhmcomulpsr 42840 evlsbagval 42848 selvvvval 42864 evlselv 42866 gicabl 43377 mendring 43466 lmodvsmdi 48661 lincvalsng 48698 lincvalsc0 48703 linc0scn0 48705 linc1 48707 lincsum 48711 lincsumcl 48713 snlindsntor 48753 grptcmon 49874 grptcepi 49875 |
| Copyright terms: Public domain | W3C validator |