![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ablgrp | Structured version Visualization version GIF version |
Description: An Abelian group is a group. (Contributed by NM, 26-Aug-2011.) |
Ref | Expression |
---|---|
ablgrp | ⊢ (𝐺 ∈ Abel → 𝐺 ∈ Grp) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | isabl 19784 | . 2 ⊢ (𝐺 ∈ Abel ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ CMnd)) | |
2 | 1 | simplbi 496 | 1 ⊢ (𝐺 ∈ Abel → 𝐺 ∈ Grp) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2099 Grpcgrp 18930 CMndccmn 19780 Abelcabl 19781 |
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 2697 |
This theorem depends on definitions: df-bi 206 df-an 395 df-tru 1537 df-ex 1775 df-sb 2061 df-clab 2704 df-cleq 2718 df-clel 2803 df-v 3464 df-in 3954 df-abl 19783 |
This theorem is referenced by: ablgrpd 19786 ablinvadd 19807 ablsub2inv 19808 ablsubadd 19809 ablsub4 19810 abladdsub4 19811 abladdsub 19812 ablsubadd23 19813 ablsubaddsub 19814 ablpncan2 19815 ablpncan3 19816 ablsubsub 19817 ablsubsub4 19818 ablpnpcan 19819 ablnncan 19820 ablnnncan 19822 ablnnncan1 19823 ablsubsub23 19824 mulgdi 19826 mulgghm 19828 mulgsubdi 19829 ghmabl 19832 invghm 19833 eqgabl 19834 odadd1 19848 odadd2 19849 odadd 19850 gexexlem 19852 gexex 19853 torsubg 19854 oddvdssubg 19855 prdsabld 19862 cnaddinv 19871 cyggexb 19899 gsumsub 19948 telgsumfzslem 19988 telgsumfzs 19989 telgsums 19993 ablfacrp 20068 ablfac1lem 20070 ablfac1b 20072 ablfac1c 20073 ablfac1eulem 20074 ablfac1eu 20075 pgpfac1lem1 20076 pgpfac1lem2 20077 pgpfac1lem3a 20078 pgpfac1lem3 20079 pgpfac1lem4 20080 pgpfac1lem5 20081 pgpfac1 20082 pgpfaclem3 20085 pgpfac 20086 ablfaclem2 20088 ablfaclem3 20089 ablfac 20090 rnglz 20150 rngpropd 20159 isringrng 20268 isrnghm 20425 isrnghmd 20435 idrnghm 20442 c0rnghm 20519 zrrnghm 20520 cnmsubglem 21429 zlmlmod 21518 frgpcyg 21573 efsubm 26581 dchrghm 27288 dchr1 27289 dchrinv 27293 dchr1re 27295 dchrpt 27299 dchrsum2 27300 sumdchr2 27302 dchrhash 27303 dchr2sum 27305 rpvmasumlem 27519 rpvmasum2 27544 dchrisum0re 27545 fedgmullem2 33527 dvalveclem 40726 primrootscoprbij 41802 primrootspoweq0 41806 isnumbasgrplem1 42780 isnumbasabl 42785 isnumbasgrp 42786 dfacbasgrp 42787 |
Copyright terms: Public domain | W3C validator |