Theorem grpmndd 19119

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  Mndcmnd 18885  Grpcgrp 19106

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-iota 6483  df-fv 6535  df-ov 7411  df-grp 19109

This theorem is used by:  grpmgmd  19134  hashfingrpnn  19145  xpsinv  19232  ghmgrp  19238  mulgdirlem  19277  ghmmhm  19402  gsumccatsymgsn  19602  symggen  19646  symgtrinv  19648  psgnunilem2  19671  psgneldm2  19680  psgnfitr  19693  lsmass  19845  frgpmhm  19941  frgpuplem  19948  frgpupf  19949  frgpup1  19951  isabld  19971  gsumzinv  20121  telgsumfzslem  20164  telgsumfzs  20165  dprdssv  20194  dprdfadd  20198  pgpfac1lem3a  20254  prdsrngd  20360  ringmnd  20432  unitabl  20576  unitsubm  20578  lmodvsmmulgdi  21134  rngqiprngimf1  21558  psgnghm  21848  rhmcomulmpl  22395  selvvvval  22413  psdmul  22449  psdmvr  22452  ply1chr  22586  clmmulg  25384  dchrptlem3  27557  abliso  33530  gsummulgc2  33561  cyc3genpmlem  33646  elrgspnsubrunlem2  33743  gsumind  33840  quslsm  33890  evl1deg1  34042  evl1deg2  34043  evl1deg3  34044  vr1nz  34059  r1pquslmic  34076  0mplrim  34080  mplmulmvr  34105  mplvrpmmhm  34112  lvecendof1f1o  34199  extdgfialglem1  34258  algextdeglem4  34286  algextdeglem5  34287  rtelextdg2lem  34292  aks6d1c6lem5  43147  rhmcomulpsr  43532  evlsbagval  43536  evlselv  43539  gicabl  44044  mendring  44133  lmodvsmdi  49413  lincvalsng  49450  lincvalsc0  49455  linc0scn0  49457  linc1  49459  lincsum  49463  lincsumcl  49465  snlindsntor  49505  grptcmon  50623  grptcepi  50624