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

Theorem ablgrp 15094
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 15093 . 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 1684   Grpcgrp 14362  CMndccmn 15089   Abelcabel 15090
This theorem is referenced by:  ablinvadd  15111  ablsub2inv  15112  ablsubadd  15113  ablsub4  15114  abladdsub4  15115  abladdsub  15116  ablpncan2  15117  ablpncan3  15118  ablsubsub  15119  ablsubsub4  15120  ablpnpcan  15121  ablnncan  15122  ablnnncan1  15124  mulgdi  15126  mulgghm  15128  mulgsubdi  15129  invghm  15130  eqgabl  15131  odadd1  15140  odadd2  15141  odadd  15142  gexexlem  15144  gexex  15145  torsubg  15146  oddvdssubg  15147  prdsabld  15154  cyggexb  15185  gsumsub  15219  ablfacrp  15301  ablfac1lem  15303  ablfac1b  15305  ablfac1c  15306  ablfac1eulem  15307  ablfac1eu  15308  pgpfac1lem1  15309  pgpfac1lem2  15310  pgpfac1lem3a  15311  pgpfac1lem3  15312  pgpfac1lem4  15313  pgpfac1lem5  15314  pgpfac1  15315  pgpfaclem3  15318  pgpfac  15319  ablfaclem2  15321  ablfaclem3  15322  ablfac  15323  cnmsubglem  16434  zlmlmod  16477  frgpcyg  16527  dchrghm  20495  dchr1  20496  dchrinv  20500  dchr1re  20502  dchrpt  20506  dchrsum2  20507  sumdchr2  20509  dchrhash  20510  dchr2sum  20512  rpvmasumlem  20636  rpvmasum2  20661  dchrisum0re  20662  isnumbasgrplem1  27266  isnumbasabl  27271  isnumbasgrp  27272  dfacbasgrp  27273  dvalveclem  31215
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-in 3159  df-abl 15092
  Copyright terms: Public domain W3C validator