![]() |
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 18583 | . 2 ⊢ (𝐺 ∈ Abel ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ CMnd)) | |
2 | 1 | simplbi 493 | 1 ⊢ (𝐺 ∈ Abel → 𝐺 ∈ Grp) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2107 Grpcgrp 17809 CMndccmn 18579 Abelcabl 18580 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-9 2116 ax-10 2135 ax-11 2150 ax-12 2163 ax-ext 2754 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-clab 2764 df-cleq 2770 df-clel 2774 df-nfc 2921 df-v 3400 df-in 3799 df-abl 18582 |
This theorem is referenced by: ablinvadd 18601 ablsub2inv 18602 ablsubadd 18603 ablsub4 18604 abladdsub4 18605 abladdsub 18606 ablpncan2 18607 ablpncan3 18608 ablsubsub 18609 ablsubsub4 18610 ablpnpcan 18611 ablnncan 18612 ablnnncan 18614 ablnnncan1 18615 ablsubsub23 18616 mulgdi 18618 mulgghm 18620 mulgsubdi 18621 ghmabl 18624 invghm 18625 eqgabl 18626 odadd1 18637 odadd2 18638 odadd 18639 gexexlem 18641 gexex 18642 torsubg 18643 oddvdssubg 18644 prdsabld 18651 cnaddinv 18660 cyggexb 18686 gsumsub 18734 telgsumfzslem 18772 telgsumfzs 18773 telgsums 18777 ablfacrp 18852 ablfac1lem 18854 ablfac1b 18856 ablfac1c 18857 ablfac1eulem 18858 ablfac1eu 18859 pgpfac1lem1 18860 pgpfac1lem2 18861 pgpfac1lem3a 18862 pgpfac1lem3 18863 pgpfac1lem4 18864 pgpfac1lem5 18865 pgpfac1 18866 pgpfaclem3 18869 pgpfac 18870 ablfaclem2 18872 ablfaclem3 18873 ablfac 18874 cnmsubglem 20205 zlmlmod 20267 frgpcyg 20317 efsubm 24735 dchrghm 25433 dchr1 25434 dchrinv 25438 dchr1re 25440 dchrpt 25444 dchrsum2 25445 sumdchr2 25447 dchrhash 25448 dchr2sum 25450 rpvmasumlem 25628 rpvmasum2 25653 dchrisum0re 25654 dvalveclem 37179 isnumbasgrplem1 38630 isnumbasabl 38635 isnumbasgrp 38636 dfacbasgrp 38637 isringrng 42896 rnglz 42899 isrnghm 42907 isrnghmd 42917 idrnghm 42923 c0rnghm 42928 zrrnghm 42932 |
Copyright terms: Public domain | W3C validator |