Theorem grpmndd 18851

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

Syntax hints:   → wi 4   ∈ wcel 2110  Mndcmnd 18634  Grpcgrp 18838

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2112  ax-9 2120  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rex 3055  df-rab 3394  df-v 3436  df-dif 3903  df-un 3905  df-ss 3917  df-nul 4282  df-if 4474  df-sn 4575  df-pr 4577  df-op 4581  df-uni 4858  df-br 5090  df-iota 6433  df-fv 6485  df-ov 7344  df-grp 18841

This theorem is referenced by:  grpmgmd  18866  hashfingrpnn  18877  xpsinv  18965  ghmgrp  18971  mulgdirlem  19010  ghmmhm  19131  gsumccatsymgsn  19331  symggen  19375  symgtrinv  19377  psgnunilem2  19400  psgneldm2  19409  psgnfitr  19422  lsmass  19574  frgpmhm  19670  frgpuplem  19677  frgpupf  19678  frgpup1  19680  isabld  19700  gsumzinv  19850  telgsumfzslem  19893  telgsumfzs  19894  dprdssv  19923  dprdfadd  19927  pgpfac1lem3a  19983  prdsrngd  20087  ringmnd  20154  unitabl  20295  unitsubm  20297  lmodvsmmulgdi  20823  rngqiprngimf1  21230  psgnghm  21510  psdmul  22074  psdmvr  22077  ply1chr  22214  rhmcomulmpl  22290  clmmulg  25021  dchrptlem3  27197  abliso  33007  gsummulgc2  33030  cyc3genpmlem  33110  elrgspnsubrunlem2  33205  gsumind  33300  quslsm  33360  evl1deg1  33529  evl1deg2  33530  evl1deg3  33531  vr1nz  33544  r1pquslmic  33561  mplvrpmmhm  33566  lvecendof1f1o  33636  extdgfialglem1  33695  algextdeglem4  33723  algextdeglem5  33724  rtelextdg2lem  33729  aks6d1c6lem5  42189  rhmcomulpsr  42563  evlsbagval  42578  selvvvval  42597  evlselv  42599  gicabl  43111  mendring  43200  lmodvsmdi  48389  lincvalsng  48427  lincvalsc0  48432  linc0scn0  48434  linc1  48436  lincsum  48440  lincsumcl  48442  snlindsntor  48482  grptcmon  49604  grptcepi  49605