Theorem grpmndd 18922

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

Syntax hints:   → wi 4   ∈ wcel 2114  Mndcmnd 18702  Grpcgrp 18909

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-iota 6455  df-fv 6507  df-ov 7370  df-grp 18912

This theorem is referenced by:  grpmgmd  18937  hashfingrpnn  18948  xpsinv  19036  ghmgrp  19042  mulgdirlem  19081  ghmmhm  19201  gsumccatsymgsn  19401  symggen  19445  symgtrinv  19447  psgnunilem2  19470  psgneldm2  19479  psgnfitr  19492  lsmass  19644  frgpmhm  19740  frgpuplem  19747  frgpupf  19748  frgpup1  19750  isabld  19770  gsumzinv  19920  telgsumfzslem  19963  telgsumfzs  19964  dprdssv  19993  dprdfadd  19997  pgpfac1lem3a  20053  prdsrngd  20157  ringmnd  20224  unitabl  20364  unitsubm  20366  lmodvsmmulgdi  20892  rngqiprngimf1  21298  psgnghm  21560  psdmul  22132  psdmvr  22135  ply1chr  22271  rhmcomulmpl  22347  clmmulg  25068  dchrptlem3  27229  abliso  33096  gsummulgc2  33127  cyc3genpmlem  33212  elrgspnsubrunlem2  33309  gsumind  33405  quslsm  33465  evl1deg1  33636  evl1deg2  33637  evl1deg3  33638  vr1nz  33653  r1pquslmic  33671  mplmulmvr  33683  mplvrpmmhm  33690  lvecendof1f1o  33777  extdgfialglem1  33836  algextdeglem4  33864  algextdeglem5  33865  rtelextdg2lem  33870  aks6d1c6lem5  42616  rhmcomulpsr  42994  evlsbagval  43002  selvvvval  43018  evlselv  43020  gicabl  43527  mendring  43616  lmodvsmdi  48849  lincvalsng  48886  lincvalsc0  48891  linc0scn0  48893  linc1  48895  lincsum  48899  lincsumcl  48901  snlindsntor  48941  grptcmon  50062  grptcepi  50063