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

Theorem ablgrp 15110
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 15109 . 2  |-  ( G  e.  Abel  <->  ( G  e. 
Grp  /\  G  e. CMnd ) )
21simplbi 446 1  |-  ( G  e.  Abel  ->  G  e. 
Grp )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1696   Grpcgrp 14378  CMndccmn 15105   Abelcabel 15106
This theorem is referenced by:  ablinvadd  15127  ablsub2inv  15128  ablsubadd  15129  ablsub4  15130  abladdsub4  15131  abladdsub  15132  ablpncan2  15133  ablpncan3  15134  ablsubsub  15135  ablsubsub4  15136  ablpnpcan  15137  ablnncan  15138  ablnnncan1  15140  mulgdi  15142  mulgghm  15144  mulgsubdi  15145  invghm  15146  eqgabl  15147  odadd1  15156  odadd2  15157  odadd  15158  gexexlem  15160  gexex  15161  torsubg  15162  oddvdssubg  15163  prdsabld  15170  cyggexb  15201  gsumsub  15235  ablfacrp  15317  ablfac1lem  15319  ablfac1b  15321  ablfac1c  15322  ablfac1eulem  15323  ablfac1eu  15324  pgpfac1lem1  15325  pgpfac1lem2  15326  pgpfac1lem3a  15327  pgpfac1lem3  15328  pgpfac1lem4  15329  pgpfac1lem5  15330  pgpfac1  15331  pgpfaclem3  15334  pgpfac  15335  ablfaclem2  15337  ablfaclem3  15338  ablfac  15339  cnmsubglem  16450  zlmlmod  16493  frgpcyg  16543  dchrghm  20511  dchr1  20512  dchrinv  20516  dchr1re  20518  dchrpt  20522  dchrsum2  20523  sumdchr2  20525  dchrhash  20526  dchr2sum  20528  rpvmasumlem  20652  rpvmasum2  20677  dchrisum0re  20678  isnumbasgrplem1  27369  isnumbasabl  27374  isnumbasgrp  27375  dfacbasgrp  27376  dvalveclem  31837
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-in 3172  df-abl 15108
  Copyright terms: Public domain W3C validator