Theorem grpmndd 18920

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

Syntax hints:   → wi 4   ∈ wcel 2119  Mndcmnd 18700  Grpcgrp 18907

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-iota 6448  df-fv 6500  df-ov 7366  df-grp 18910

This theorem is referenced by:  grpmgmd  18935  hashfingrpnn  18946  xpsinv  19034  ghmgrp  19040  mulgdirlem  19079  ghmmhm  19199  gsumccatsymgsn  19399  symggen  19443  symgtrinv  19445  psgnunilem2  19468  psgneldm2  19477  psgnfitr  19490  lsmass  19642  frgpmhm  19738  frgpuplem  19745  frgpupf  19746  frgpup1  19748  isabld  19768  gsumzinv  19918  telgsumfzslem  19961  telgsumfzs  19962  dprdssv  19991  dprdfadd  19995  pgpfac1lem3a  20051  prdsrngd  20155  ringmnd  20222  unitabl  20362  unitsubm  20364  lmodvsmmulgdi  20894  rngqiprngimf1  21300  psgnghm  21562  rhmcomulmpl  22107  selvvvval  22125  psdmul  22161  psdmvr  22164  ply1chr  22299  clmmulg  25093  dchrptlem3  27254  abliso  33122  gsummulgc2  33154  cyc3genpmlem  33239  elrgspnsubrunlem2  33336  gsumind  33435  quslsm  33495  evl1deg1  33666  evl1deg2  33667  evl1deg3  33668  vr1nz  33683  r1pquslmic  33701  0mplrim  33705  mplmulmvr  33730  mplvrpmmhm  33737  lvecendof1f1o  33824  extdgfialglem1  33883  algextdeglem4  33911  algextdeglem5  33912  rtelextdg2lem  33917  aks6d1c6lem5  42663  rhmcomulpsr  43033  evlsbagval  43037  evlselv  43040  gicabl  43545  mendring  43634  lmodvsmdi  48871  lincvalsng  48908  lincvalsc0  48913  linc0scn0  48915  linc1  48917  lincsum  48921  lincsumcl  48923  snlindsntor  48963  grptcmon  50084  grptcepi  50085