| 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 19802 | . 2 ⊢ (𝐺 ∈ Abel ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ CMnd)) | |
| 2 | 1 | simplbi 497 | 1 ⊢ (𝐺 ∈ Abel → 𝐺 ∈ Grp) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∈ wcel 2108 Grpcgrp 18951 CMndccmn 19798 Abelcabl 19799 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-v 3482 df-in 3958 df-abl 19801 |
| This theorem is referenced by: ablgrpd 19804 ablinvadd 19825 ablsub2inv 19826 ablsubadd 19827 ablsub4 19828 abladdsub4 19829 abladdsub 19830 ablsubadd23 19831 ablsubaddsub 19832 ablpncan2 19833 ablpncan3 19834 ablsubsub 19835 ablsubsub4 19836 ablpnpcan 19837 ablnncan 19838 ablnnncan 19840 ablnnncan1 19841 ablsubsub23 19842 mulgdi 19844 mulgghm 19846 mulgsubdi 19847 ghmabl 19850 invghm 19851 eqgabl 19852 odadd1 19866 odadd2 19867 odadd 19868 gexexlem 19870 gexex 19871 torsubg 19872 oddvdssubg 19873 prdsabld 19880 cnaddinv 19889 cyggexb 19917 gsumsub 19966 telgsumfzslem 20006 telgsumfzs 20007 telgsums 20011 ablfacrp 20086 ablfac1lem 20088 ablfac1b 20090 ablfac1c 20091 ablfac1eulem 20092 ablfac1eu 20093 pgpfac1lem1 20094 pgpfac1lem2 20095 pgpfac1lem3a 20096 pgpfac1lem3 20097 pgpfac1lem4 20098 pgpfac1lem5 20099 pgpfac1 20100 pgpfaclem3 20103 pgpfac 20104 ablfaclem2 20106 ablfaclem3 20107 ablfac 20108 rnglz 20162 rngpropd 20171 isringrng 20284 isrnghm 20441 isrnghmd 20451 idrnghm 20458 c0rnghm 20535 zrrnghm 20536 cnmsubglem 21448 zlmlmod 21537 frgpcyg 21592 efsubm 26593 dchrghm 27300 dchr1 27301 dchrinv 27305 dchr1re 27307 dchrpt 27311 dchrsum2 27312 sumdchr2 27314 dchrhash 27315 dchr2sum 27317 rpvmasumlem 27531 rpvmasum2 27556 dchrisum0re 27557 fedgmullem2 33681 dvalveclem 41027 primrootscoprbij 42103 primrootspoweq0 42107 isnumbasgrplem1 43113 isnumbasabl 43118 isnumbasgrp 43119 dfacbasgrp 43120 |
| Copyright terms: Public domain | W3C validator |