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

Theorem ablgrp 15419
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 15418 . 2  |-  ( G  e.  Abel  <->  ( G  e. 
Grp  /\  G  e. CMnd ) )
21simplbi 448 1  |-  ( G  e.  Abel  ->  G  e. 
Grp )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1726   Grpcgrp 14687  CMndccmn 15414   Abelcabel 15415
This theorem is referenced by:  ablinvadd  15436  ablsub2inv  15437  ablsubadd  15438  ablsub4  15439  abladdsub4  15440  abladdsub  15441  ablpncan2  15442  ablpncan3  15443  ablsubsub  15444  ablsubsub4  15445  ablpnpcan  15446  ablnncan  15447  ablnnncan1  15449  mulgdi  15451  mulgghm  15453  mulgsubdi  15454  invghm  15455  eqgabl  15456  odadd1  15465  odadd2  15466  odadd  15467  gexexlem  15469  gexex  15470  torsubg  15471  oddvdssubg  15472  prdsabld  15479  cyggexb  15510  gsumsub  15544  ablfacrp  15626  ablfac1lem  15628  ablfac1b  15630  ablfac1c  15631  ablfac1eulem  15632  ablfac1eu  15633  pgpfac1lem1  15634  pgpfac1lem2  15635  pgpfac1lem3a  15636  pgpfac1lem3  15637  pgpfac1lem4  15638  pgpfac1lem5  15639  pgpfac1  15640  pgpfaclem3  15643  pgpfac  15644  ablfaclem2  15646  ablfaclem3  15647  ablfac  15648  cnmsubglem  16763  zlmlmod  16806  frgpcyg  16856  dchrghm  21042  dchr1  21043  dchrinv  21047  dchr1re  21049  dchrpt  21053  dchrsum2  21054  sumdchr2  21056  dchrhash  21057  dchr2sum  21059  rpvmasumlem  21183  rpvmasum2  21208  dchrisum0re  21209  isnumbasgrplem1  27245  isnumbasabl  27250  isnumbasgrp  27251  dfacbasgrp  27252  dvalveclem  31885
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-v 2960  df-in 3329  df-abl 15417
  Copyright terms: Public domain W3C validator