grpmndd - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > grpmndd		Structured version Visualization version GIF version

Theorem grpmndd 18896

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

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∈ wcel 2099 Mndcmnd 18687 Grpcgrp 18883

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2699

This theorem depends on definitions: df-bi 206 df-an 396 df-or 847 df-3an 1087 df-tru 1537 df-fal 1547 df-ex 1775 df-sb 2061 df-clab 2706 df-cleq 2720 df-clel 2806 df-ral 3058 df-rex 3067 df-rab 3429 df-v 3472 df-dif 3948 df-un 3950 df-in 3952 df-ss 3962 df-nul 4319 df-if 4525 df-sn 4625 df-pr 4627 df-op 4631 df-uni 4904 df-br 5143 df-iota 6494 df-fv 6550 df-ov 7417 df-grp 18886

This theorem is referenced by: grpmgmd 18911 hashfingrpnn 18922 xpsinv 19009 ghmgrp 19015 mulgdirlem 19053 ghmmhm 19173 gsumccatsymgsn 19374 symggen 19418 symgtrinv 19420 psgnunilem2 19443 psgneldm2 19452 psgnfitr 19465 lsmass 19617 frgpmhm 19713 frgpuplem 19720 frgpupf 19721 frgpup1 19723 isabld 19743 gsumzinv 19893 telgsumfzslem 19936 telgsumfzs 19937 dprdssv 19966 dprdfadd 19970 pgpfac1lem3a 20026 prdsrngd 20109 ringmnd 20176 unitabl 20316 unitsubm 20318 lmodvsmmulgdi 20773 rngqiprngimf1 21183 psgnghm 21505 psdmul 22083 ply1chr 22218 clmmulg 25021 dchrptlem3 27192 abliso 32750 cyc3genpmlem 32866 quslsm 33109 r1pquslmic 33271 algextdeglem4 33382 algextdeglem5 33383 aks6d1c6lem5 41643 rhmcomulmpl 41779 evlsbagval 41793 selvvvval 41812 evlselv 41814 gicabl 42517 mendring 42610 lmodvsmdi 47440 lincvalsng 47478 lincvalsc0 47483 linc0scn0 47485 linc1 47487 lincsum 47491 lincsumcl 47493 snlindsntor 47533 grptcmon 48096 grptcepi 48097

	
		OSZAR »