Theorem grpmndd 18828

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

Syntax hints:   → wi 4   ∈ wcel 2106  Mndcmnd 18621  Grpcgrp 18815

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-iota 6492  df-fv 6548  df-ov 7408  df-grp 18818

This theorem is referenced by:  hashfingrpnn  18853  ghmgrp  18943  mulgdirlem  18979  ghmmhm  19096  gsumccatsymgsn  19288  symggen  19332  symgtrinv  19334  psgnunilem2  19357  psgneldm2  19366  psgnfitr  19379  lsmass  19531  frgpmhm  19627  frgpuplem  19634  frgpupf  19635  frgpup1  19637  isabld  19657  gsumzinv  19807  telgsumfzslem  19850  telgsumfzs  19851  dprdssv  19880  dprdfadd  19884  pgpfac1lem3a  19940  ringmnd  20059  unitabl  20190  unitsubm  20192  lmodvsmmulgdi  20499  psgnghm  21124  clmmulg  24608  dchrptlem3  26758  abliso  32184  cyc3genpmlem  32297  quslsm  32504  ply1chr  32649  algextdeglem1  32760  rhmcomulmpl  41121  evlsbagval  41135  selvvvval  41154  evlselv  41156  gicabl  41826  mendring  41919  prdsrngd  46663  rngqiprngimf1  46765  lmodvsmdi  47011  lincvalsng  47050  lincvalsc0  47055  linc0scn0  47057  linc1  47059  lincsum  47063  lincsumcl  47065  snlindsntor  47105  grptcmon  47669  grptcepi  47670