Theorem grpmndd 18868

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

Syntax hints:   → wi 4   ∈ wcel 2106  Mndcmnd 18659  Grpcgrp 18855

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 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-iota 6495  df-fv 6551  df-ov 7414  df-grp 18858

This theorem is referenced by:  hashfingrpnn  18893  xpsinv  18979  ghmgrp  18985  mulgdirlem  19021  ghmmhm  19140  gsumccatsymgsn  19335  symggen  19379  symgtrinv  19381  psgnunilem2  19404  psgneldm2  19413  psgnfitr  19426  lsmass  19578  frgpmhm  19674  frgpuplem  19681  frgpupf  19682  frgpup1  19684  isabld  19704  gsumzinv  19854  telgsumfzslem  19897  telgsumfzs  19898  dprdssv  19927  dprdfadd  19931  pgpfac1lem3a  19987  prdsrngd  20070  ringmnd  20137  unitabl  20275  unitsubm  20277  lmodvsmmulgdi  20651  rngqiprngimf1  21059  psgnghm  21352  clmmulg  24841  dchrptlem3  26993  abliso  32452  cyc3genpmlem  32568  quslsm  32778  ply1chr  32923  r1pquslmic  32944  algextdeglem4  33053  algextdeglem5  33054  rhmcomulmpl  41426  evlsbagval  41440  selvvvval  41459  evlselv  41461  gicabl  42143  mendring  42236  lmodvsmdi  47147  lincvalsng  47185  lincvalsc0  47190  linc0scn0  47192  linc1  47194  lincsum  47198  lincsumcl  47200  snlindsntor  47240  grptcmon  47804  grptcepi  47805