Theorem grpmndd 18911

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 18905	. 2 ⊢ (𝐺 ∈ Grp → 𝐺 ∈ Mnd)
3	1, 2	syl 17	1 ⊢ (𝜑 → 𝐺 ∈ Mnd)

Syntax hints:   → wi 4   ∈ wcel 2114  Mndcmnd 18691  Grpcgrp 18898

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 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-iota 6446  df-fv 6498  df-ov 7361  df-grp 18901

This theorem is referenced by:  grpmgmd  18926  hashfingrpnn  18937  xpsinv  19025  ghmgrp  19031  mulgdirlem  19070  ghmmhm  19190  gsumccatsymgsn  19390  symggen  19434  symgtrinv  19436  psgnunilem2  19459  psgneldm2  19468  psgnfitr  19481  lsmass  19633  frgpmhm  19729  frgpuplem  19736  frgpupf  19737  frgpup1  19739  isabld  19759  gsumzinv  19909  telgsumfzslem  19952  telgsumfzs  19953  dprdssv  19982  dprdfadd  19986  pgpfac1lem3a  20042  prdsrngd  20146  ringmnd  20213  unitabl  20353  unitsubm  20355  lmodvsmmulgdi  20881  rngqiprngimf1  21288  psgnghm  21568  psdmul  22141  psdmvr  22144  ply1chr  22280  rhmcomulmpl  22356  clmmulg  25077  dchrptlem3  27248  abliso  33116  gsummulgc2  33147  cyc3genpmlem  33232  elrgspnsubrunlem2  33329  gsumind  33425  quslsm  33485  evl1deg1  33656  evl1deg2  33657  evl1deg3  33658  vr1nz  33673  r1pquslmic  33691  mplmulmvr  33703  mplvrpmmhm  33710  lvecendof1f1o  33798  extdgfialglem1  33857  algextdeglem4  33885  algextdeglem5  33886  rtelextdg2lem  33891  aks6d1c6lem5  42627  rhmcomulpsr  43005  evlsbagval  43013  selvvvval  43029  evlselv  43031  gicabl  43542  mendring  43631  lmodvsmdi  48852  lincvalsng  48889  lincvalsc0  48894  linc0scn0  48896  linc1  48898  lincsum  48902  lincsumcl  48904  snlindsntor  48944  grptcmon  50065  grptcepi  50066