Theorem grpmndd 18807

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

Syntax hints:   → wi 4   ∈ wcel 2106  Mndcmnd 18602  Grpcgrp 18794

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-ral 3061  df-rex 3070  df-rab 3432  df-v 3475  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4319  df-if 4523  df-sn 4623  df-pr 4625  df-op 4629  df-uni 4902  df-br 5142  df-iota 6484  df-fv 6540  df-ov 7396  df-grp 18797

This theorem is referenced by:  hashfingrpnn  18832  ghmgrp  18921  mulgdirlem  18957  ghmmhm  19068  gsumccatsymgsn  19258  symggen  19302  symgtrinv  19304  psgnunilem2  19327  psgneldm2  19336  psgnfitr  19349  lsmass  19501  frgpmhm  19597  frgpuplem  19604  frgpupf  19605  frgpup1  19607  isabld  19627  gsumzinv  19772  telgsumfzslem  19815  telgsumfzs  19816  dprdssv  19845  dprdfadd  19849  pgpfac1lem3a  19905  ringmnd  20024  unitabl  20150  unitsubm  20152  lmodvsmmulgdi  20456  psgnghm  21066  clmmulg  24546  dchrptlem3  26696  abliso  32068  cyc3genpmlem  32181  quslsm  32374  ply1chr  32501  rhmcomulmpl  40926  evlsbagval  40934  gicabl  41612  mendring  41705  lmodvsmdi  46706  lincvalsng  46745  lincvalsc0  46750  linc0scn0  46752  linc1  46754  lincsum  46758  lincsumcl  46760  snlindsntor  46800  grptcmon  47364  grptcepi  47365