Theorem grpmndd 19012

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

Syntax hints:   → wi 4   ∈ wcel 2141  Mndcmnd 18791  Grpcgrp 18999

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1571  df-fal 1581  df-ex 1808  df-sb 2095  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rex 3088  df-rab 3415  df-v 3455  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4487  df-sn 4589  df-pr 4591  df-op 4595  df-uni 4872  df-br 5109  df-iota 6492  df-fv 6544  df-ov 7413  df-grp 19002

This theorem is referenced by:  grpmgmd  19027  hashfingrpnn  19038  xpsinv  19125  ghmgrp  19131  mulgdirlem  19170  ghmmhm  19295  gsumccatsymgsn  19495  symggen  19539  symgtrinv  19541  psgnunilem2  19564  psgneldm2  19573  psgnfitr  19586  lsmass  19738  frgpmhm  19834  frgpuplem  19841  frgpupf  19842  frgpup1  19844  isabld  19864  gsumzinv  20014  telgsumfzslem  20057  telgsumfzs  20058  dprdssv  20087  dprdfadd  20091  pgpfac1lem3a  20147  prdsrngd  20253  ringmnd  20324  unitabl  20465  unitsubm  20467  lmodvsmmulgdi  20997  rngqiprngimf1  21419  psgnghm  21709  rhmcomulmpl  22254  selvvvval  22272  psdmul  22308  psdmvr  22311  ply1chr  22445  clmmulg  25239  dchrptlem3  27406  abliso  33321  gsummulgc2  33352  cyc3genpmlem  33437  elrgspnsubrunlem2  33534  gsumind  33631  quslsm  33680  evl1deg1  33832  evl1deg2  33833  evl1deg3  33834  vr1nz  33849  r1pquslmic  33866  0mplrim  33870  mplmulmvr  33895  mplvrpmmhm  33902  lvecendof1f1o  33989  extdgfialglem1  34048  algextdeglem4  34076  algextdeglem5  34077  rtelextdg2lem  34082  aks6d1c6lem5  42912  rhmcomulpsr  43284  evlsbagval  43288  evlselv  43291  gicabl  43796  mendring  43885  lmodvsmdi  49126  lincvalsng  49163  lincvalsc0  49168  linc0scn0  49170  linc1  49172  lincsum  49176  lincsumcl  49178  snlindsntor  49218  grptcmon  50338  grptcepi  50339