Theorem grpmndd 18377

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

Syntax hints:   → wi 4   ∈ wcel 2110  Mndcmnd 18173  Grpcgrp 18365

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3410  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-nul 4238  df-if 4440  df-sn 4542  df-pr 4544  df-op 4548  df-uni 4820  df-br 5054  df-iota 6338  df-fv 6388  df-ov 7216  df-grp 18368

This theorem is referenced by:  hashfingrpnn  18400  ghmgrp  18487  mulgdirlem  18522  ghmmhm  18632  gsumccatsymgsn  18818  symggen  18862  symgtrinv  18864  psgnunilem2  18887  psgneldm2  18896  psgnfitr  18909  lsmass  19059  frgpmhm  19155  frgpuplem  19162  frgpupf  19163  frgpup1  19165  isabld  19184  gsumzinv  19330  telgsumfzslem  19373  telgsumfzs  19374  dprdssv  19403  dprdfadd  19407  pgpfac1lem3a  19463  ringmnd  19572  unitabl  19686  unitsubm  19688  lmodvsmmulgdi  19934  psgnghm  20542  clmmulg  23998  dchrptlem3  26147  abliso  31024  cyc3genpmlem  31137  quslsm  31307  ply1chr  31383  evlsbagval  39985  gicabl  40627  mendring  40720  lmodvsmdi  45391  lincvalsng  45430  lincvalsc0  45435  linc0scn0  45437  linc1  45439  lincsum  45443  lincsumcl  45445  snlindsntor  45485  grptcmon  46048  grptcepi  46049