Theorem grpmndd 18869

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

Syntax hints:   → wi 4   ∈ wcel 2113  Mndcmnd 18652  Grpcgrp 18856

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 2115  ax-9 2123  ax-ext 2705

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 2712  df-cleq 2725  df-clel 2808  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-br 5096  df-iota 6445  df-fv 6497  df-ov 7358  df-grp 18859

This theorem is referenced by:  grpmgmd  18884  hashfingrpnn  18895  xpsinv  18983  ghmgrp  18989  mulgdirlem  19028  ghmmhm  19148  gsumccatsymgsn  19348  symggen  19392  symgtrinv  19394  psgnunilem2  19417  psgneldm2  19426  psgnfitr  19439  lsmass  19591  frgpmhm  19687  frgpuplem  19694  frgpupf  19695  frgpup1  19697  isabld  19717  gsumzinv  19867  telgsumfzslem  19910  telgsumfzs  19911  dprdssv  19940  dprdfadd  19944  pgpfac1lem3a  20000  prdsrngd  20104  ringmnd  20171  unitabl  20312  unitsubm  20314  lmodvsmmulgdi  20840  rngqiprngimf1  21247  psgnghm  21527  psdmul  22091  psdmvr  22094  ply1chr  22231  rhmcomulmpl  22307  clmmulg  25038  dchrptlem3  27214  abliso  33028  gsummulgc2  33051  cyc3genpmlem  33131  elrgspnsubrunlem2  33226  gsumind  33321  quslsm  33381  evl1deg1  33550  evl1deg2  33551  evl1deg3  33552  vr1nz  33565  r1pquslmic  33582  mplvrpmmhm  33587  lvecendof1f1o  33657  extdgfialglem1  33716  algextdeglem4  33744  algextdeglem5  33745  rtelextdg2lem  33750  aks6d1c6lem5  42280  rhmcomulpsr  42659  evlsbagval  42674  selvvvval  42693  evlselv  42695  gicabl  43206  mendring  43295  lmodvsmdi  48493  lincvalsng  48531  lincvalsc0  48536  linc0scn0  48538  linc1  48540  lincsum  48544  lincsumcl  48546  snlindsntor  48586  grptcmon  49708  grptcepi  49709