ablgrp - Metamath Proof Explorer

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

Theorem ablgrp 19739

Description: An Abelian group is a group. (Contributed by NM, 26-Aug-2011.)

**Assertion**
Ref	Expression
ablgrp	⊢ (𝐺 ∈ Abel → 𝐺 ∈ Grp)

**Proof of Theorem ablgrp**
Step	Hyp	Ref	Expression
1		isabl 19738	. 2 ⊢ (𝐺 ∈ Abel ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ CMnd))
2	1	simplbi 497	1 ⊢ (𝐺 ∈ Abel → 𝐺 ∈ Grp)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∈ wcel 2099 Grpcgrp 18889 CMndccmn 19734 Abelcabl 19735

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-tru 1537 df-ex 1775 df-sb 2061 df-clab 2706 df-cleq 2720 df-clel 2806 df-v 3473 df-in 3954 df-abl 19737

This theorem is referenced by: ablgrpd 19740 ablinvadd 19761 ablsub2inv 19762 ablsubadd 19763 ablsub4 19764 abladdsub4 19765 abladdsub 19766 ablsubadd23 19767 ablsubaddsub 19768 ablpncan2 19769 ablpncan3 19770 ablsubsub 19771 ablsubsub4 19772 ablpnpcan 19773 ablnncan 19774 ablnnncan 19776 ablnnncan1 19777 ablsubsub23 19778 mulgdi 19780 mulgghm 19782 mulgsubdi 19783 ghmabl 19786 invghm 19787 eqgabl 19788 odadd1 19802 odadd2 19803 odadd 19804 gexexlem 19806 gexex 19807 torsubg 19808 oddvdssubg 19809 prdsabld 19816 cnaddinv 19825 cyggexb 19853 gsumsub 19902 telgsumfzslem 19942 telgsumfzs 19943 telgsums 19947 ablfacrp 20022 ablfac1lem 20024 ablfac1b 20026 ablfac1c 20027 ablfac1eulem 20028 ablfac1eu 20029 pgpfac1lem1 20030 pgpfac1lem2 20031 pgpfac1lem3a 20032 pgpfac1lem3 20033 pgpfac1lem4 20034 pgpfac1lem5 20035 pgpfac1 20036 pgpfaclem3 20039 pgpfac 20040 ablfaclem2 20042 ablfaclem3 20043 ablfac 20044 rnglz 20104 rngpropd 20113 isringrng 20222 isrnghm 20379 isrnghmd 20389 idrnghm 20396 c0rnghm 20471 zrrnghm 20472 cnmsubglem 21362 zlmlmod 21451 frgpcyg 21506 efsubm 26484 dchrghm 27188 dchr1 27189 dchrinv 27193 dchr1re 27195 dchrpt 27199 dchrsum2 27200 sumdchr2 27202 dchrhash 27203 dchr2sum 27205 rpvmasumlem 27419 rpvmasum2 27444 dchrisum0re 27445 fedgmullem2 33324 dvalveclem 40498 primrootscoprbij 41573 primrootspoweq0 41577 isnumbasgrplem1 42525 isnumbasabl 42530 isnumbasgrp 42531 dfacbasgrp 42532

	
		OSZAR »