Theorem grpmndd 18859

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

Syntax hints:   → wi 4   ∈ wcel 2111  Mndcmnd 18642  Grpcgrp 18846

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-br 5090  df-iota 6437  df-fv 6489  df-ov 7349  df-grp 18849

This theorem is referenced by:  grpmgmd  18874  hashfingrpnn  18885  xpsinv  18973  ghmgrp  18979  mulgdirlem  19018  ghmmhm  19138  gsumccatsymgsn  19338  symggen  19382  symgtrinv  19384  psgnunilem2  19407  psgneldm2  19416  psgnfitr  19429  lsmass  19581  frgpmhm  19677  frgpuplem  19684  frgpupf  19685  frgpup1  19687  isabld  19707  gsumzinv  19857  telgsumfzslem  19900  telgsumfzs  19901  dprdssv  19930  dprdfadd  19934  pgpfac1lem3a  19990  prdsrngd  20094  ringmnd  20161  unitabl  20302  unitsubm  20304  lmodvsmmulgdi  20830  rngqiprngimf1  21237  psgnghm  21517  psdmul  22081  psdmvr  22084  ply1chr  22221  rhmcomulmpl  22297  clmmulg  25028  dchrptlem3  27204  abliso  33017  gsummulgc2  33040  cyc3genpmlem  33120  elrgspnsubrunlem2  33215  gsumind  33310  quslsm  33370  evl1deg1  33539  evl1deg2  33540  evl1deg3  33541  vr1nz  33554  r1pquslmic  33571  mplvrpmmhm  33576  lvecendof1f1o  33646  extdgfialglem1  33705  algextdeglem4  33733  algextdeglem5  33734  rtelextdg2lem  33739  aks6d1c6lem5  42269  rhmcomulpsr  42643  evlsbagval  42658  selvvvval  42677  evlselv  42679  gicabl  43191  mendring  43280  lmodvsmdi  48478  lincvalsng  48516  lincvalsc0  48521  linc0scn0  48523  linc1  48525  lincsum  48529  lincsumcl  48531  snlindsntor  48571  grptcmon  49693  grptcepi  49694