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 18841 | . 2 ⊢ (𝐺 ∈ Abel ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ CMnd)) | |
2 | 1 | simplbi 498 | 1 ⊢ (𝐺 ∈ Abel → 𝐺 ∈ Grp) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2105 Grpcgrp 18043 CMndccmn 18837 Abelcabl 18838 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2793 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-v 3497 df-in 3942 df-abl 18840 |
This theorem is referenced by: ablgrpd 18843 ablinvadd 18861 ablsub2inv 18862 ablsubadd 18863 ablsub4 18864 abladdsub4 18865 abladdsub 18866 ablpncan2 18867 ablpncan3 18868 ablsubsub 18869 ablsubsub4 18870 ablpnpcan 18871 ablnncan 18872 ablnnncan 18874 ablnnncan1 18875 ablsubsub23 18876 mulgdi 18878 mulgghm 18880 mulgsubdi 18881 ghmabl 18884 invghm 18885 eqgabl 18886 odadd1 18899 odadd2 18900 odadd 18901 gexexlem 18903 gexex 18904 torsubg 18905 oddvdssubg 18906 prdsabld 18913 cnaddinv 18922 cyggexb 18950 gsumsub 18999 telgsumfzslem 19039 telgsumfzs 19040 telgsums 19044 ablfacrp 19119 ablfac1lem 19121 ablfac1b 19123 ablfac1c 19124 ablfac1eulem 19125 ablfac1eu 19126 pgpfac1lem1 19127 pgpfac1lem2 19128 pgpfac1lem3a 19129 pgpfac1lem3 19130 pgpfac1lem4 19131 pgpfac1lem5 19132 pgpfac1 19133 pgpfaclem3 19136 pgpfac 19137 ablfaclem2 19139 ablfaclem3 19140 ablfac 19141 cnmsubglem 20538 zlmlmod 20600 frgpcyg 20650 efsubm 25062 dchrghm 25760 dchr1 25761 dchrinv 25765 dchr1re 25767 dchrpt 25771 dchrsum2 25772 sumdchr2 25774 dchrhash 25775 dchr2sum 25777 rpvmasumlem 25991 rpvmasum2 26016 dchrisum0re 26017 fedgmullem2 30926 dvalveclem 38043 isnumbasgrplem1 39581 isnumbasabl 39586 isnumbasgrp 39587 dfacbasgrp 39588 isringrng 44050 rnglz 44053 isrnghm 44061 isrnghmd 44071 idrnghm 44077 c0rnghm 44082 zrrnghm 44086 |
Copyright terms: Public domain | W3C validator |