Theorem grpmndd 18934

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

Syntax hints:   → wi 4   ∈ wcel 2109  Mndcmnd 18717  Grpcgrp 18921

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-ral 3053  df-rex 3062  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-br 5125  df-iota 6489  df-fv 6544  df-ov 7413  df-grp 18924

This theorem is referenced by:  grpmgmd  18949  hashfingrpnn  18960  xpsinv  19048  ghmgrp  19054  mulgdirlem  19093  ghmmhm  19214  gsumccatsymgsn  19412  symggen  19456  symgtrinv  19458  psgnunilem2  19481  psgneldm2  19490  psgnfitr  19503  lsmass  19655  frgpmhm  19751  frgpuplem  19758  frgpupf  19759  frgpup1  19761  isabld  19781  gsumzinv  19931  telgsumfzslem  19974  telgsumfzs  19975  dprdssv  20004  dprdfadd  20008  pgpfac1lem3a  20064  prdsrngd  20141  ringmnd  20208  unitabl  20349  unitsubm  20351  lmodvsmmulgdi  20859  rngqiprngimf1  21266  psgnghm  21545  psdmul  22109  psdmvr  22112  ply1chr  22249  rhmcomulmpl  22325  clmmulg  25057  dchrptlem3  27234  abliso  33036  gsummulgc2  33059  cyc3genpmlem  33167  elrgspnsubrunlem2  33248  quslsm  33425  evl1deg1  33594  evl1deg2  33595  evl1deg3  33596  vr1nz  33608  r1pquslmic  33625  lvecendof1f1o  33678  algextdeglem4  33759  algextdeglem5  33760  rtelextdg2lem  33765  aks6d1c6lem5  42195  rhmcomulpsr  42541  evlsbagval  42556  selvvvval  42575  evlselv  42577  gicabl  43090  mendring  43179  lmodvsmdi  48321  lincvalsng  48359  lincvalsc0  48364  linc0scn0  48366  linc1  48368  lincsum  48372  lincsumcl  48374  snlindsntor  48414  grptcmon  49437  grptcepi  49438