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 18913 | . 2 ⊢ (𝐺 ∈ Abel ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ CMnd)) | |
2 | 1 | simplbi 500 | 1 ⊢ (𝐺 ∈ Abel → 𝐺 ∈ Grp) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2113 Grpcgrp 18106 CMndccmn 18909 Abelcabl 18910 |
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 1969 ax-7 2014 ax-8 2115 ax-9 2123 ax-10 2144 ax-11 2160 ax-12 2176 ax-ext 2796 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-tru 1539 df-ex 1780 df-nf 1784 df-sb 2069 df-clab 2803 df-cleq 2817 df-clel 2896 df-nfc 2966 df-v 3499 df-in 3946 df-abl 18912 |
This theorem is referenced by: ablgrpd 18915 ablinvadd 18933 ablsub2inv 18934 ablsubadd 18935 ablsub4 18936 abladdsub4 18937 abladdsub 18938 ablpncan2 18939 ablpncan3 18940 ablsubsub 18941 ablsubsub4 18942 ablpnpcan 18943 ablnncan 18944 ablnnncan 18946 ablnnncan1 18947 ablsubsub23 18948 mulgdi 18950 mulgghm 18952 mulgsubdi 18953 ghmabl 18956 invghm 18957 eqgabl 18958 odadd1 18971 odadd2 18972 odadd 18973 gexexlem 18975 gexex 18976 torsubg 18977 oddvdssubg 18978 prdsabld 18985 cnaddinv 18994 cyggexb 19022 gsumsub 19071 telgsumfzslem 19111 telgsumfzs 19112 telgsums 19116 ablfacrp 19191 ablfac1lem 19193 ablfac1b 19195 ablfac1c 19196 ablfac1eulem 19197 ablfac1eu 19198 pgpfac1lem1 19199 pgpfac1lem2 19200 pgpfac1lem3a 19201 pgpfac1lem3 19202 pgpfac1lem4 19203 pgpfac1lem5 19204 pgpfac1 19205 pgpfaclem3 19208 pgpfac 19209 ablfaclem2 19211 ablfaclem3 19212 ablfac 19213 cnmsubglem 20611 zlmlmod 20673 frgpcyg 20723 efsubm 25138 dchrghm 25835 dchr1 25836 dchrinv 25840 dchr1re 25842 dchrpt 25846 dchrsum2 25847 sumdchr2 25849 dchrhash 25850 dchr2sum 25852 rpvmasumlem 26066 rpvmasum2 26091 dchrisum0re 26092 fedgmullem2 31030 dvalveclem 38165 isnumbasgrplem1 39707 isnumbasabl 39712 isnumbasgrp 39713 dfacbasgrp 39714 isringrng 44159 rnglz 44162 isrnghm 44170 isrnghmd 44180 idrnghm 44186 c0rnghm 44191 zrrnghm 44195 |
Copyright terms: Public domain | W3C validator |