MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  grpmndd Structured version   Visualization version   GIF version

Theorem grpmndd 18761
Description: A group is a monoid. (Contributed by SN, 1-Jun-2024.)
Hypothesis
Ref Expression
grpmndd.1 (𝜑𝐺 ∈ Grp)
Assertion
Ref Expression
grpmndd (𝜑𝐺 ∈ Mnd)

Proof of Theorem grpmndd
StepHypRef Expression
1 grpmndd.1 . 2 (𝜑𝐺 ∈ Grp)
2 grpmnd 18756 . 2 (𝐺 ∈ Grp → 𝐺 ∈ Mnd)
31, 2syl 17 1 (𝜑𝐺 ∈ Mnd)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107  Mndcmnd 18557  Grpcgrp 18749
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-ral 3066  df-rex 3075  df-rab 3409  df-v 3448  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-br 5107  df-iota 6449  df-fv 6505  df-ov 7361  df-grp 18752
This theorem is referenced by:  hashfingrpnn  18784  ghmgrp  18872  mulgdirlem  18908  ghmmhm  19019  gsumccatsymgsn  19209  symggen  19253  symgtrinv  19255  psgnunilem2  19278  psgneldm2  19287  psgnfitr  19300  lsmass  19452  frgpmhm  19548  frgpuplem  19555  frgpupf  19556  frgpup1  19558  isabld  19578  gsumzinv  19723  telgsumfzslem  19766  telgsumfzs  19767  dprdssv  19796  dprdfadd  19800  pgpfac1lem3a  19856  ringmnd  19975  unitabl  20098  unitsubm  20100  lmodvsmmulgdi  20360  psgnghm  20987  clmmulg  24467  dchrptlem3  26617  abliso  31890  cyc3genpmlem  32003  quslsm  32189  ply1chr  32285  rhmcomulmpl  40743  evlsbagval  40751  gicabl  41429  mendring  41522  lmodvsmdi  46465  lincvalsng  46504  lincvalsc0  46509  linc0scn0  46511  linc1  46513  lincsum  46517  lincsumcl  46519  snlindsntor  46559  grptcmon  47123  grptcepi  47124
  Copyright terms: Public domain W3C validator