Theorem grpmndd 18504

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

Syntax hints:   → wi 4   ∈ wcel 2108  Mndcmnd 18300  Grpcgrp 18492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-iota 6376  df-fv 6426  df-ov 7258  df-grp 18495

This theorem is referenced by:  hashfingrpnn  18527  ghmgrp  18614  mulgdirlem  18649  ghmmhm  18759  gsumccatsymgsn  18949  symggen  18993  symgtrinv  18995  psgnunilem2  19018  psgneldm2  19027  psgnfitr  19040  lsmass  19190  frgpmhm  19286  frgpuplem  19293  frgpupf  19294  frgpup1  19296  isabld  19315  gsumzinv  19461  telgsumfzslem  19504  telgsumfzs  19505  dprdssv  19534  dprdfadd  19538  pgpfac1lem3a  19594  ringmnd  19708  unitabl  19825  unitsubm  19827  lmodvsmmulgdi  20073  psgnghm  20697  clmmulg  24170  dchrptlem3  26319  abliso  31207  cyc3genpmlem  31320  quslsm  31495  ply1chr  31571  evlsbagval  40198  gicabl  40840  mendring  40933  lmodvsmdi  45606  lincvalsng  45645  lincvalsc0  45650  linc0scn0  45652  linc1  45654  lincsum  45658  lincsumcl  45660  snlindsntor  45700  grptcmon  46263  grptcepi  46264