Theorem grpmndd 18880

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

Syntax hints:   → wi 4   ∈ wcel 2114  Mndcmnd 18663  Grpcgrp 18867

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 3062  df-rab 3401  df-v 3443  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4287  df-if 4481  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-iota 6449  df-fv 6501  df-ov 7363  df-grp 18870

This theorem is referenced by:  grpmgmd  18895  hashfingrpnn  18906  xpsinv  18994  ghmgrp  19000  mulgdirlem  19039  ghmmhm  19159  gsumccatsymgsn  19359  symggen  19403  symgtrinv  19405  psgnunilem2  19428  psgneldm2  19437  psgnfitr  19450  lsmass  19602  frgpmhm  19698  frgpuplem  19705  frgpupf  19706  frgpup1  19708  isabld  19728  gsumzinv  19878  telgsumfzslem  19921  telgsumfzs  19922  dprdssv  19951  dprdfadd  19955  pgpfac1lem3a  20011  prdsrngd  20115  ringmnd  20182  unitabl  20324  unitsubm  20326  lmodvsmmulgdi  20852  rngqiprngimf1  21259  psgnghm  21539  psdmul  22113  psdmvr  22116  ply1chr  22254  rhmcomulmpl  22330  clmmulg  25061  dchrptlem3  27237  abliso  33099  gsummulgc2  33130  cyc3genpmlem  33214  elrgspnsubrunlem2  33311  gsumind  33407  quslsm  33467  evl1deg1  33638  evl1deg2  33639  evl1deg3  33640  vr1nz  33655  r1pquslmic  33673  mplmulmvr  33685  mplvrpmmhm  33692  lvecendof1f1o  33771  extdgfialglem1  33830  algextdeglem4  33858  algextdeglem5  33859  rtelextdg2lem  33864  aks6d1c6lem5  42468  rhmcomulpsr  42840  evlsbagval  42848  selvvvval  42864  evlselv  42866  gicabl  43377  mendring  43466  lmodvsmdi  48661  lincvalsng  48698  lincvalsc0  48703  linc0scn0  48705  linc1  48707  lincsum  48711  lincsumcl  48713  snlindsntor  48753  grptcmon  49874  grptcepi  49875