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

Theorem ablgrp 16282
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 16281 . 2  |-  ( G  e.  Abel  <->  ( G  e. 
Grp  /\  G  e. CMnd ) )
21simplbi 460 1  |-  ( G  e.  Abel  ->  G  e. 
Grp )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1756   Grpcgrp 15410  CMndccmn 16277   Abelcabel 16278
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-v 2974  df-in 3335  df-abl 16280
This theorem is referenced by:  ablinvadd  16299  ablsub2inv  16300  ablsubadd  16301  ablsub4  16302  abladdsub4  16303  abladdsub  16304  ablpncan2  16305  ablpncan3  16306  ablsubsub  16307  ablsubsub4  16308  ablpnpcan  16309  ablnncan  16310  ablnnncan1  16312  mulgdi  16314  mulgghm  16316  mulgsubdi  16317  invghm  16318  eqgabl  16319  odadd1  16330  odadd2  16331  odadd  16332  gexexlem  16334  gexex  16335  torsubg  16336  oddvdssubg  16337  prdsabld  16344  cyggexb  16375  gsumsub  16447  gsumsubOLD  16448  ablfacrp  16567  ablfac1lem  16569  ablfac1b  16571  ablfac1c  16572  ablfac1eulem  16573  ablfac1eu  16574  pgpfac1lem1  16575  pgpfac1lem2  16576  pgpfac1lem3a  16577  pgpfac1lem3  16578  pgpfac1lem4  16579  pgpfac1lem5  16580  pgpfac1  16581  pgpfaclem3  16584  pgpfac  16585  ablfaclem2  16587  ablfaclem3  16588  ablfac  16589  cnmsubglem  17875  zlmlmod  17954  frgpcyg  18006  dchrghm  22595  dchr1  22596  dchrinv  22600  dchr1re  22602  dchrpt  22606  dchrsum2  22607  sumdchr2  22609  dchrhash  22610  dchr2sum  22612  rpvmasumlem  22736  rpvmasum2  22761  dchrisum0re  22762  isnumbasgrplem1  29457  isnumbasabl  29462  isnumbasgrp  29463  dfacbasgrp  29464  telescfzgsumlem  30809  telescfzgsum  30810  telescgsum  30811  dvalveclem  34670
  Copyright terms: Public domain W3C validator