| 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 18853 | . 2 ⊢ (𝐺 ∈ Grp → 𝐺 ∈ Mnd) | |
| 3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → 𝐺 ∈ Mnd) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∈ wcel 2111 Mndcmnd 18642 Grpcgrp 18846 |
| 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 |
| 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-ral 3048 df-rex 3057 df-rab 3396 df-v 3438 df-dif 3900 df-un 3902 df-ss 3914 df-nul 4281 df-if 4473 df-sn 4574 df-pr 4576 df-op 4580 df-uni 4857 df-br 5090 df-iota 6437 df-fv 6489 df-ov 7349 df-grp 18849 |
| This theorem is referenced by: grpmgmd 18874 hashfingrpnn 18885 xpsinv 18973 ghmgrp 18979 mulgdirlem 19018 ghmmhm 19138 gsumccatsymgsn 19338 symggen 19382 symgtrinv 19384 psgnunilem2 19407 psgneldm2 19416 psgnfitr 19429 lsmass 19581 frgpmhm 19677 frgpuplem 19684 frgpupf 19685 frgpup1 19687 isabld 19707 gsumzinv 19857 telgsumfzslem 19900 telgsumfzs 19901 dprdssv 19930 dprdfadd 19934 pgpfac1lem3a 19990 prdsrngd 20094 ringmnd 20161 unitabl 20302 unitsubm 20304 lmodvsmmulgdi 20830 rngqiprngimf1 21237 psgnghm 21517 psdmul 22081 psdmvr 22084 ply1chr 22221 rhmcomulmpl 22297 clmmulg 25028 dchrptlem3 27204 abliso 33017 gsummulgc2 33040 cyc3genpmlem 33120 elrgspnsubrunlem2 33215 gsumind 33310 quslsm 33370 evl1deg1 33539 evl1deg2 33540 evl1deg3 33541 vr1nz 33554 r1pquslmic 33571 mplvrpmmhm 33576 lvecendof1f1o 33646 extdgfialglem1 33705 algextdeglem4 33733 algextdeglem5 33734 rtelextdg2lem 33739 aks6d1c6lem5 42269 rhmcomulpsr 42643 evlsbagval 42658 selvvvval 42677 evlselv 42679 gicabl 43191 mendring 43280 lmodvsmdi 48478 lincvalsng 48516 lincvalsc0 48521 linc0scn0 48523 linc1 48525 lincsum 48529 lincsumcl 48531 snlindsntor 48571 grptcmon 49693 grptcepi 49694 |
| Copyright terms: Public domain | W3C validator |