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

Theorem ablgrp 19496
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 19495 . 2 (𝐺 ∈ Abel ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ CMnd))
21simplbi 498 1 (𝐺 ∈ Abel → 𝐺 ∈ Grp)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2106  Grpcgrp 18682  CMndccmn 19491  Abelcabl 19492
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3445  df-in 3915  df-abl 19494
This theorem is referenced by:  ablgrpd  19497  ablinvadd  19517  ablsub2inv  19518  ablsubadd  19519  ablsub4  19520  abladdsub4  19521  abladdsub  19522  ablpncan2  19523  ablpncan3  19524  ablsubsub  19525  ablsubsub4  19526  ablpnpcan  19527  ablnncan  19528  ablnnncan  19530  ablnnncan1  19531  ablsubsub23  19532  mulgdi  19534  mulgghm  19536  mulgsubdi  19537  ghmabl  19540  invghm  19541  eqgabl  19542  odadd1  19555  odadd2  19556  odadd  19557  gexexlem  19559  gexex  19560  torsubg  19561  oddvdssubg  19562  prdsabld  19569  cnaddinv  19578  cyggexb  19605  gsumsub  19654  telgsumfzslem  19694  telgsumfzs  19695  telgsums  19699  ablfacrp  19774  ablfac1lem  19776  ablfac1b  19778  ablfac1c  19779  ablfac1eulem  19780  ablfac1eu  19781  pgpfac1lem1  19782  pgpfac1lem2  19783  pgpfac1lem3a  19784  pgpfac1lem3  19785  pgpfac1lem4  19786  pgpfac1lem5  19787  pgpfac1  19788  pgpfaclem3  19791  pgpfac  19792  ablfaclem2  19794  ablfaclem3  19795  ablfac  19796  cnmsubglem  20783  zlmlmod  20850  frgpcyg  20903  efsubm  25829  dchrghm  26526  dchr1  26527  dchrinv  26531  dchr1re  26533  dchrpt  26537  dchrsum2  26538  sumdchr2  26540  dchrhash  26541  dchr2sum  26543  rpvmasumlem  26757  rpvmasum2  26782  dchrisum0re  26783  fedgmullem2  32108  dvalveclem  39383  isnumbasgrplem1  41293  isnumbasabl  41298  isnumbasgrp  41299  dfacbasgrp  41300  isringrng  45928  rnglz  45931  isrnghm  45939  isrnghmd  45949  idrnghm  45955  c0rnghm  45960  zrrnghm  45964
  Copyright terms: Public domain W3C validator