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

Theorem ablgrp 17019
Description: An Abelian group is a group. (Contributed by NM, 26-Aug-2011.)
Assertion
Ref Expression
ablgrp  |-  ( G  e.  Abel  ->  G  e. 
Grp )

Proof of Theorem ablgrp
StepHypRef Expression
1 isabl 17018 . 2  |-  ( G  e.  Abel  <->  ( G  e. 
Grp  /\  G  e. CMnd ) )
21simplbi 458 1  |-  ( G  e.  Abel  ->  G  e. 
Grp )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1842   Grpcgrp 16269  CMndccmn 17014   Abelcabl 17015
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-v 3060  df-in 3420  df-abl 17017
This theorem is referenced by:  ablinvadd  17036  ablsub2inv  17037  ablsubadd  17038  ablsub4  17039  abladdsub4  17040  abladdsub  17041  ablpncan2  17042  ablpncan3  17043  ablsubsub  17044  ablsubsub4  17045  ablpnpcan  17046  ablnncan  17047  ablnnncan1  17049  mulgdi  17051  mulgghm  17053  mulgsubdi  17054  ghmabl  17057  invghm  17058  eqgabl  17059  odadd1  17070  odadd2  17071  odadd  17072  gexexlem  17074  gexex  17075  torsubg  17076  oddvdssubg  17077  prdsabld  17084  cyggexb  17117  gsumsub  17188  telgsumfzslem  17229  telgsumfzs  17230  telgsums  17234  ablfacrp  17329  ablfac1lem  17331  ablfac1b  17333  ablfac1c  17334  ablfac1eulem  17335  ablfac1eu  17336  pgpfac1lem1  17337  pgpfac1lem2  17338  pgpfac1lem3a  17339  pgpfac1lem3  17340  pgpfac1lem4  17341  pgpfac1lem5  17342  pgpfac1  17343  pgpfaclem3  17346  pgpfac  17347  ablfaclem2  17349  ablfaclem3  17350  ablfac  17351  cnmsubglem  18692  zlmlmod  18752  frgpcyg  18802  efsubm  23122  dchrghm  23804  dchr1  23805  dchrinv  23809  dchr1re  23811  dchrpt  23815  dchrsum2  23816  sumdchr2  23818  dchrhash  23819  dchr2sum  23821  rpvmasumlem  23945  rpvmasum2  23970  dchrisum0re  23971  dvalveclem  34026  isnumbasgrplem1  35395  isnumbasabl  35400  isnumbasgrp  35401  dfacbasgrp  35402  isringrng  38178  rnglz  38181  isrnghm  38189  isrnghmd  38199  idrnghm  38205  c0rnghm  38210  zrrnghm  38214
  Copyright terms: Public domain W3C validator