Theorem grpmndd 19074

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  Mndcmnd 18840  Grpcgrp 19061

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 2734

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 2741  df-cleq 2754  df-clel 2837  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-iota 6493  df-fv 6545  df-ov 7419  df-grp 19064

This theorem is used by:  grpmgmd  19089  hashfingrpnn  19100  xpsinv  19187  ghmgrp  19193  mulgdirlem  19232  ghmmhm  19357  gsumccatsymgsn  19557  symggen  19601  symgtrinv  19603  psgnunilem2  19626  psgneldm2  19635  psgnfitr  19648  lsmass  19800  frgpmhm  19896  frgpuplem  19903  frgpupf  19904  frgpup1  19906  isabld  19926  gsumzinv  20076  telgsumfzslem  20119  telgsumfzs  20120  dprdssv  20149  dprdfadd  20153  pgpfac1lem3a  20209  prdsrngd  20315  ringmnd  20386  unitabl  20529  unitsubm  20531  lmodvsmmulgdi  21085  rngqiprngimf1  21507  psgnghm  21797  rhmcomulmpl  22344  selvvvval  22362  psdmul  22398  psdmvr  22401  ply1chr  22535  clmmulg  25333  dchrptlem3  27503  abliso  33477  gsummulgc2  33508  cyc3genpmlem  33593  elrgspnsubrunlem2  33690  gsumind  33787  quslsm  33836  evl1deg1  33988  evl1deg2  33989  evl1deg3  33990  vr1nz  34005  r1pquslmic  34022  0mplrim  34026  mplmulmvr  34051  mplvrpmmhm  34058  lvecendof1f1o  34145  extdgfialglem1  34204  algextdeglem4  34232  algextdeglem5  34233  rtelextdg2lem  34238  aks6d1c6lem5  43045  rhmcomulpsr  43430  evlsbagval  43434  evlselv  43437  gicabl  43942  mendring  44031  lmodvsmdi  49311  lincvalsng  49348  lincvalsc0  49353  linc0scn0  49355  linc1  49357  lincsum  49361  lincsumcl  49363  snlindsntor  49403  grptcmon  50521  grptcepi  50522