Theorem grpmndd 18976

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

Syntax hints:   → wi 4   ∈ wcel 2105  Mndcmnd 18759  Grpcgrp 18963

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-iota 6515  df-fv 6570  df-ov 7433  df-grp 18966

This theorem is referenced by:  grpmgmd  18991  hashfingrpnn  19002  xpsinv  19090  ghmgrp  19096  mulgdirlem  19135  ghmmhm  19256  gsumccatsymgsn  19458  symggen  19502  symgtrinv  19504  psgnunilem2  19527  psgneldm2  19536  psgnfitr  19549  lsmass  19701  frgpmhm  19797  frgpuplem  19804  frgpupf  19805  frgpup1  19807  isabld  19827  gsumzinv  19977  telgsumfzslem  20020  telgsumfzs  20021  dprdssv  20050  dprdfadd  20054  pgpfac1lem3a  20110  prdsrngd  20193  ringmnd  20260  unitabl  20400  unitsubm  20402  lmodvsmmulgdi  20911  rngqiprngimf1  21327  psgnghm  21615  psdmul  22187  ply1chr  22325  rhmcomulmpl  22401  clmmulg  25147  dchrptlem3  27324  abliso  33023  gsummulgc2  33045  cyc3genpmlem  33153  quslsm  33412  evl1deg1  33580  evl1deg2  33581  evl1deg3  33582  r1pquslmic  33610  lvecendof1f1o  33660  algextdeglem4  33725  algextdeglem5  33726  rtelextdg2lem  33731  aks6d1c6lem5  42158  rhmcomulpsr  42537  evlsbagval  42552  selvvvval  42571  evlselv  42573  gicabl  43087  mendring  43176  lmodvsmdi  48223  lincvalsng  48261  lincvalsc0  48266  linc0scn0  48268  linc1  48270  lincsum  48274  lincsumcl  48276  snlindsntor  48316  grptcmon  48901  grptcepi  48902