Theorem grpmndd 18885

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

Syntax hints:   → wi 4   ∈ wcel 2109  Mndcmnd 18668  Grpcgrp 18872

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-iota 6467  df-fv 6522  df-ov 7393  df-grp 18875

This theorem is referenced by:  grpmgmd  18900  hashfingrpnn  18911  xpsinv  18999  ghmgrp  19005  mulgdirlem  19044  ghmmhm  19165  gsumccatsymgsn  19363  symggen  19407  symgtrinv  19409  psgnunilem2  19432  psgneldm2  19441  psgnfitr  19454  lsmass  19606  frgpmhm  19702  frgpuplem  19709  frgpupf  19710  frgpup1  19712  isabld  19732  gsumzinv  19882  telgsumfzslem  19925  telgsumfzs  19926  dprdssv  19955  dprdfadd  19959  pgpfac1lem3a  20015  prdsrngd  20092  ringmnd  20159  unitabl  20300  unitsubm  20302  lmodvsmmulgdi  20810  rngqiprngimf1  21217  psgnghm  21496  psdmul  22060  psdmvr  22063  ply1chr  22200  rhmcomulmpl  22276  clmmulg  25008  dchrptlem3  27184  abliso  32984  gsummulgc2  33007  cyc3genpmlem  33115  elrgspnsubrunlem2  33206  quslsm  33383  evl1deg1  33552  evl1deg2  33553  evl1deg3  33554  vr1nz  33566  r1pquslmic  33583  lvecendof1f1o  33636  algextdeglem4  33717  algextdeglem5  33718  rtelextdg2lem  33723  aks6d1c6lem5  42172  rhmcomulpsr  42546  evlsbagval  42561  selvvvval  42580  evlselv  42582  gicabl  43095  mendring  43184  lmodvsmdi  48371  lincvalsng  48409  lincvalsc0  48414  linc0scn0  48416  linc1  48418  lincsum  48422  lincsumcl  48424  snlindsntor  48464  grptcmon  49586  grptcepi  49587