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 499 1 (𝐺 ∈ Abel → 𝐺 ∈ Grp)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107  Grpcgrp 18683  CMndccmn 19491  Abelcabl 19492
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2709
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3446  df-in 3916  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  32096  dvalveclem  39374  isnumbasgrplem1  41262  isnumbasabl  41267  isnumbasgrp  41268  dfacbasgrp  41269  isringrng  45879  rnglz  45882  isrnghm  45890  isrnghmd  45900  idrnghm  45906  c0rnghm  45911  zrrnghm  45915
  Copyright terms: Public domain W3C validator