Theorem grpmndd 19158

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  Mndcmnd 18924  Grpcgrp 19145

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-iota 6494  df-fv 6546  df-ov 7423  df-grp 19148

This theorem is used by:  grpmgmd  19173  hashfingrpnn  19184  xpsinv  19271  ghmgrp  19277  mulgdirlem  19316  ghmmhm  19441  gsumccatsymgsn  19641  symggen  19685  symgtrinv  19687  psgnunilem2  19710  psgneldm2  19719  psgnfitr  19732  lsmass  19884  frgpmhm  19980  frgpuplem  19987  frgpupf  19988  frgpup1  19990  isabld  20010  gsumzinv  20160  telgsumfzslem  20203  telgsumfzs  20204  dprdssv  20233  dprdfadd  20237  pgpfac1lem3a  20293  prdsrngd  20399  ringmnd  20471  unitabl  20615  unitsubm  20617  lmodvsmmulgdi  21173  rngqiprngimf1  21597  psgnghm  21887  rhmcomulmpl  22434  selvvvval  22452  psdmul  22488  psdmvr  22491  ply1chr  22625  clmmulg  25423  dchrptlem3  27594  abliso  33639  gsummulgc2  33670  cyc3genpmlem  33755  elrgspnsubrunlem2  33852  gsumind  33949  quslsm  33999  evl1deg1  34151  evl1deg2  34152  evl1deg3  34153  vr1nz  34168  r1pquslmic  34185  0mplrim  34189  mplmulmvr  34214  mplvrpmmhm  34221  lvecendof1f1o  34308  extdgfialglem1  34367  algextdeglem4  34395  algextdeglem5  34396  rtelextdg2lem  34401  aks6d1c6lem5  43303  rhmcomulpsr  43686  evlsbagval  43690  evlselv  43693  gicabl  44177  mendring  44266  lmodvsmdi  49567  lincvalsng  49604  lincvalsc0  49609  linc0scn0  49611  linc1  49613  lincsum  49617  lincsumcl  49619  snlindsntor  49659  grptcmon  50777  grptcepi  50778