Theorem grpmndd 19003

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

Step	Hyp	Ref	Expression
1		grpmndd.1	. 2 ⊢ (𝜑 → 𝐺 ∈ Grp)
2		grpmnd 18997	. 2 ⊢ (𝐺 ∈ Grp → 𝐺 ∈ Mnd)
3	1, 2	syl 18	1 ⊢ (𝜑 → 𝐺 ∈ Mnd)

Syntax hints:   → wi 4   ∈ wcel 2145  Mndcmnd 18782  Grpcgrp 18990

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4869  df-br 5106  df-iota 6481  df-fv 6533  df-ov 7403  df-grp 18993

This theorem is referenced by:  grpmgmd  19018  hashfingrpnn  19029  xpsinv  19117  ghmgrp  19123  mulgdirlem  19162  ghmmhm  19287  gsumccatsymgsn  19487  symggen  19531  symgtrinv  19533  psgnunilem2  19556  psgneldm2  19565  psgnfitr  19578  lsmass  19730  frgpmhm  19826  frgpuplem  19833  frgpupf  19834  frgpup1  19836  isabld  19856  gsumzinv  20006  telgsumfzslem  20049  telgsumfzs  20050  dprdssv  20079  dprdfadd  20083  pgpfac1lem3a  20139  prdsrngd  20245  ringmnd  20316  unitabl  20457  unitsubm  20459  lmodvsmmulgdi  20987  rngqiprngimf1  21402  psgnghm  21690  rhmcomulmpl  22235  selvvvval  22253  psdmul  22289  psdmvr  22292  ply1chr  22427  clmmulg  25221  dchrptlem3  27388  abliso  33268  gsummulgc2  33299  cyc3genpmlem  33384  elrgspnsubrunlem2  33481  gsumind  33580  quslsm  33630  evl1deg1  33783  evl1deg2  33784  evl1deg3  33785  vr1nz  33800  r1pquslmic  33817  0mplrim  33821  mplmulmvr  33846  mplvrpmmhm  33853  lvecendof1f1o  33940  extdgfialglem1  33999  algextdeglem4  34027  algextdeglem5  34028  rtelextdg2lem  34033  aks6d1c6lem5  42806  rhmcomulpsr  43176  evlsbagval  43180  evlselv  43183  gicabl  43688  mendring  43777  lmodvsmdi  49010  lincvalsng  49047  lincvalsc0  49052  linc0scn0  49054  linc1  49056  lincsum  49060  lincsumcl  49062  snlindsntor  49102  grptcmon  50222  grptcepi  50223