Theorem grpmndd 18964

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

Syntax hints:   → wi 4   ∈ wcel 2108  Mndcmnd 18747  Grpcgrp 18951

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-iota 6514  df-fv 6569  df-ov 7434  df-grp 18954

This theorem is referenced by:  grpmgmd  18979  hashfingrpnn  18990  xpsinv  19078  ghmgrp  19084  mulgdirlem  19123  ghmmhm  19244  gsumccatsymgsn  19444  symggen  19488  symgtrinv  19490  psgnunilem2  19513  psgneldm2  19522  psgnfitr  19535  lsmass  19687  frgpmhm  19783  frgpuplem  19790  frgpupf  19791  frgpup1  19793  isabld  19813  gsumzinv  19963  telgsumfzslem  20006  telgsumfzs  20007  dprdssv  20036  dprdfadd  20040  pgpfac1lem3a  20096  prdsrngd  20173  ringmnd  20240  unitabl  20384  unitsubm  20386  lmodvsmmulgdi  20895  rngqiprngimf1  21310  psgnghm  21598  psdmul  22170  psdmvr  22173  ply1chr  22310  rhmcomulmpl  22386  clmmulg  25134  dchrptlem3  27310  abliso  33041  gsummulgc2  33063  cyc3genpmlem  33171  elrgspnsubrunlem2  33252  quslsm  33433  evl1deg1  33601  evl1deg2  33602  evl1deg3  33603  r1pquslmic  33631  lvecendof1f1o  33684  algextdeglem4  33761  algextdeglem5  33762  rtelextdg2lem  33767  aks6d1c6lem5  42178  rhmcomulpsr  42561  evlsbagval  42576  selvvvval  42595  evlselv  42597  gicabl  43111  mendring  43200  lmodvsmdi  48295  lincvalsng  48333  lincvalsc0  48338  linc0scn0  48340  linc1  48342  lincsum  48346  lincsumcl  48348  snlindsntor  48388  grptcmon  49190  grptcepi  49191