Theorem grpmndd 19019

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2142  Mndcmnd 18798  Grpcgrp 19006

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1104  df-tru 1572  df-fal 1582  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-ral 3079  df-rex 3089  df-rab 3416  df-v 3456  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 7415  df-grp 19009

This theorem is used by:  grpmgmd  19034  hashfingrpnn  19045  xpsinv  19132  ghmgrp  19138  mulgdirlem  19177  ghmmhm  19302  gsumccatsymgsn  19502  symggen  19546  symgtrinv  19548  psgnunilem2  19571  psgneldm2  19580  psgnfitr  19593  lsmass  19745  frgpmhm  19841  frgpuplem  19848  frgpupf  19849  frgpup1  19851  isabld  19871  gsumzinv  20021  telgsumfzslem  20064  telgsumfzs  20065  dprdssv  20094  dprdfadd  20098  pgpfac1lem3a  20154  prdsrngd  20260  ringmnd  20331  unitabl  20473  unitsubm  20475  lmodvsmmulgdi  21029  rngqiprngimf1  21451  psgnghm  21741  rhmcomulmpl  22286  selvvvval  22304  psdmul  22340  psdmvr  22343  ply1chr  22477  clmmulg  25271  dchrptlem3  27441  abliso  33364  gsummulgc2  33395  cyc3genpmlem  33480  elrgspnsubrunlem2  33577  gsumind  33674  quslsm  33723  evl1deg1  33875  evl1deg2  33876  evl1deg3  33877  vr1nz  33892  r1pquslmic  33909  0mplrim  33913  mplmulmvr  33938  mplvrpmmhm  33945  lvecendof1f1o  34032  extdgfialglem1  34091  algextdeglem4  34119  algextdeglem5  34120  rtelextdg2lem  34125  aks6d1c6lem5  42972  rhmcomulpsr  43342  evlsbagval  43346  evlselv  43349  gicabl  43854  mendring  43943  lmodvsmdi  49187  lincvalsng  49224  lincvalsc0  49229  linc0scn0  49231  linc1  49233  lincsum  49237  lincsumcl  49239  snlindsntor  49279  grptcmon  50399  grptcepi  50400