Theorem grpmndd 18843

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

Syntax hints:   → wi 4   ∈ wcel 2109  Mndcmnd 18626  Grpcgrp 18830

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 2701

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 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-iota 6442  df-fv 6494  df-ov 7356  df-grp 18833

This theorem is referenced by:  grpmgmd  18858  hashfingrpnn  18869  xpsinv  18957  ghmgrp  18963  mulgdirlem  19002  ghmmhm  19123  gsumccatsymgsn  19323  symggen  19367  symgtrinv  19369  psgnunilem2  19392  psgneldm2  19401  psgnfitr  19414  lsmass  19566  frgpmhm  19662  frgpuplem  19669  frgpupf  19670  frgpup1  19672  isabld  19692  gsumzinv  19842  telgsumfzslem  19885  telgsumfzs  19886  dprdssv  19915  dprdfadd  19919  pgpfac1lem3a  19975  prdsrngd  20079  ringmnd  20146  unitabl  20287  unitsubm  20289  lmodvsmmulgdi  20818  rngqiprngimf1  21225  psgnghm  21505  psdmul  22069  psdmvr  22072  ply1chr  22209  rhmcomulmpl  22285  clmmulg  25017  dchrptlem3  27193  abliso  33003  gsummulgc2  33026  cyc3genpmlem  33106  elrgspnsubrunlem2  33198  quslsm  33352  evl1deg1  33521  evl1deg2  33522  evl1deg3  33523  vr1nz  33535  r1pquslmic  33552  lvecendof1f1o  33605  algextdeglem4  33686  algextdeglem5  33687  rtelextdg2lem  33692  aks6d1c6lem5  42150  rhmcomulpsr  42524  evlsbagval  42539  selvvvval  42558  evlselv  42560  gicabl  43072  mendring  43161  lmodvsmdi  48351  lincvalsng  48389  lincvalsc0  48394  linc0scn0  48396  linc1  48398  lincsum  48402  lincsumcl  48404  snlindsntor  48444  grptcmon  49566  grptcepi  49567