Theorem grpmndd 18589

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

Syntax hints:   → wi 4   ∈ wcel 2106  Mndcmnd 18385  Grpcgrp 18577

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-iota 6391  df-fv 6441  df-ov 7278  df-grp 18580

This theorem is referenced by:  hashfingrpnn  18612  ghmgrp  18699  mulgdirlem  18734  ghmmhm  18844  gsumccatsymgsn  19034  symggen  19078  symgtrinv  19080  psgnunilem2  19103  psgneldm2  19112  psgnfitr  19125  lsmass  19275  frgpmhm  19371  frgpuplem  19378  frgpupf  19379  frgpup1  19381  isabld  19400  gsumzinv  19546  telgsumfzslem  19589  telgsumfzs  19590  dprdssv  19619  dprdfadd  19623  pgpfac1lem3a  19679  ringmnd  19793  unitabl  19910  unitsubm  19912  lmodvsmmulgdi  20158  psgnghm  20785  clmmulg  24264  dchrptlem3  26414  abliso  31305  cyc3genpmlem  31418  quslsm  31593  ply1chr  31669  evlsbagval  40275  gicabl  40924  mendring  41017  lmodvsmdi  45718  lincvalsng  45757  lincvalsc0  45762  linc0scn0  45764  linc1  45766  lincsum  45770  lincsumcl  45772  snlindsntor  45812  grptcmon  46377  grptcepi  46378