MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ablgrp Structured version   Visualization version   GIF version

Theorem ablgrp 18130
Description: An Abelian group is a group. (Contributed by NM, 26-Aug-2011.)
Assertion
Ref Expression
ablgrp (𝐺 ∈ Abel → 𝐺 ∈ Grp)

Proof of Theorem ablgrp
StepHypRef Expression
1 isabl 18129 . 2 (𝐺 ∈ Abel ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ CMnd))
21simplbi 476 1 (𝐺 ∈ Abel → 𝐺 ∈ Grp)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1987  Grpcgrp 17354  CMndccmn 18125  Abelcabl 18126
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-v 3191  df-in 3566  df-abl 18128
This theorem is referenced by:  ablinvadd  18147  ablsub2inv  18148  ablsubadd  18149  ablsub4  18150  abladdsub4  18151  abladdsub  18152  ablpncan2  18153  ablpncan3  18154  ablsubsub  18155  ablsubsub4  18156  ablpnpcan  18157  ablnncan  18158  ablnnncan  18160  ablnnncan1  18161  ablsubsub23  18162  mulgdi  18164  mulgghm  18166  mulgsubdi  18167  ghmabl  18170  invghm  18171  eqgabl  18172  odadd1  18183  odadd2  18184  odadd  18185  gexexlem  18187  gexex  18188  torsubg  18189  oddvdssubg  18190  prdsabld  18197  cnaddinv  18206  cyggexb  18232  gsumsub  18280  telgsumfzslem  18317  telgsumfzs  18318  telgsums  18322  ablfacrp  18397  ablfac1lem  18399  ablfac1b  18401  ablfac1c  18402  ablfac1eulem  18403  ablfac1eu  18404  pgpfac1lem1  18405  pgpfac1lem2  18406  pgpfac1lem3a  18407  pgpfac1lem3  18408  pgpfac1lem4  18409  pgpfac1lem5  18410  pgpfac1  18411  pgpfaclem3  18414  pgpfac  18415  ablfaclem2  18417  ablfaclem3  18418  ablfac  18419  cnmsubglem  19741  zlmlmod  19803  frgpcyg  19854  efsubm  24218  dchrghm  24898  dchr1  24899  dchrinv  24903  dchr1re  24905  dchrpt  24909  dchrsum2  24910  sumdchr2  24912  dchrhash  24913  dchr2sum  24915  rpvmasumlem  25093  rpvmasum2  25118  dchrisum0re  25119  dvalveclem  35829  isnumbasgrplem1  37187  isnumbasabl  37192  isnumbasgrp  37193  dfacbasgrp  37194  isringrng  41195  rnglz  41198  isrnghm  41206  isrnghmd  41216  idrnghm  41222  c0rnghm  41227  zrrnghm  41231
  Copyright terms: Public domain W3C validator