![]() |
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 18801 | . 2 ⊢ (𝐺 ∈ Grp → 𝐺 ∈ Mnd) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → 𝐺 ∈ Mnd) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2106 Mndcmnd 18602 Grpcgrp 18794 |
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 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2702 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-sb 2068 df-clab 2709 df-cleq 2723 df-clel 2809 df-ral 3061 df-rex 3070 df-rab 3432 df-v 3475 df-dif 3947 df-un 3949 df-in 3951 df-ss 3961 df-nul 4319 df-if 4523 df-sn 4623 df-pr 4625 df-op 4629 df-uni 4902 df-br 5142 df-iota 6484 df-fv 6540 df-ov 7396 df-grp 18797 |
This theorem is referenced by: hashfingrpnn 18832 ghmgrp 18921 mulgdirlem 18957 ghmmhm 19068 gsumccatsymgsn 19258 symggen 19302 symgtrinv 19304 psgnunilem2 19327 psgneldm2 19336 psgnfitr 19349 lsmass 19501 frgpmhm 19597 frgpuplem 19604 frgpupf 19605 frgpup1 19607 isabld 19627 gsumzinv 19772 telgsumfzslem 19815 telgsumfzs 19816 dprdssv 19845 dprdfadd 19849 pgpfac1lem3a 19905 ringmnd 20024 unitabl 20150 unitsubm 20152 lmodvsmmulgdi 20456 psgnghm 21066 clmmulg 24546 dchrptlem3 26696 abliso 32068 cyc3genpmlem 32181 quslsm 32374 ply1chr 32501 rhmcomulmpl 40926 evlsbagval 40934 gicabl 41612 mendring 41705 lmodvsmdi 46706 lincvalsng 46745 lincvalsc0 46750 linc0scn0 46752 linc1 46754 lincsum 46758 lincsumcl 46760 snlindsntor 46800 grptcmon 47364 grptcepi 47365 |
Copyright terms: Public domain | W3C validator |