Theorem grpmndd 18964

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

Syntax hints:   → wi 4   ∈ wcel 2136  Mndcmnd 18744  Grpcgrp 18951

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1809  ax-4 1823  ax-5 1924  ax-6 1981  ax-7 2022  ax-8 2138  ax-9 2146  ax-ext 2728

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-3an 1097  df-tru 1557  df-fal 1567  df-ex 1794  df-sb 2085  df-clab 2735  df-cleq 2748  df-clel 2831  df-ral 3071  df-rex 3081  df-rab 3409  df-v 3450  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4281  df-if 4475  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5095  df-iota 6466  df-fv 6518  df-ov 7388  df-grp 18954

This theorem is referenced by:  grpmgmd  18979  hashfingrpnn  18990  xpsinv  19078  ghmgrp  19084  mulgdirlem  19123  ghmmhm  19242  gsumccatsymgsn  19442  symggen  19486  symgtrinv  19488  psgnunilem2  19511  psgneldm2  19520  psgnfitr  19533  lsmass  19685  frgpmhm  19781  frgpuplem  19788  frgpupf  19789  frgpup1  19791  isabld  19811  gsumzinv  19961  telgsumfzslem  20004  telgsumfzs  20005  dprdssv  20034  dprdfadd  20038  pgpfac1lem3a  20094  prdsrngd  20198  ringmnd  20265  unitabl  20405  unitsubm  20407  lmodvsmmulgdi  20937  rngqiprngimf1  21343  psgnghm  21605  rhmcomulmpl  22150  selvvvval  22168  psdmul  22204  psdmvr  22207  ply1chr  22342  clmmulg  25136  dchrptlem3  27300  abliso  33168  gsummulgc2  33200  cyc3genpmlem  33285  elrgspnsubrunlem2  33383  gsumind  33485  quslsm  33545  evl1deg1  33726  evl1deg2  33727  evl1deg3  33728  vr1nz  33743  r1pquslmic  33761  0mplrim  33765  mplmulmvr  33790  mplvrpmmhm  33797  lvecendof1f1o  33884  extdgfialglem1  33943  algextdeglem4  33971  algextdeglem5  33972  rtelextdg2lem  33977  aks6d1c6lem5  42742  rhmcomulpsr  43112  evlsbagval  43116  evlselv  43119  gicabl  43624  mendring  43713  lmodvsmdi  48949  lincvalsng  48986  lincvalsc0  48991  linc0scn0  48993  linc1  48995  lincsum  48999  lincsumcl  49001  snlindsntor  49041  grptcmon  50162  grptcepi  50163