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

Theorem ablgrp 16596
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 16595 . 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 1767   Grpcgrp 15720  CMndccmn 16591   Abelcabl 16592
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3115  df-in 3483  df-abl 16594
This theorem is referenced by:  ablinvadd  16613  ablsub2inv  16614  ablsubadd  16615  ablsub4  16616  abladdsub4  16617  abladdsub  16618  ablpncan2  16619  ablpncan3  16620  ablsubsub  16621  ablsubsub4  16622  ablpnpcan  16623  ablnncan  16624  ablnnncan1  16626  mulgdi  16628  mulgghm  16630  mulgsubdi  16631  invghm  16632  eqgabl  16633  odadd1  16644  odadd2  16645  odadd  16646  gexexlem  16648  gexex  16649  torsubg  16650  oddvdssubg  16651  prdsabld  16658  cyggexb  16689  gsumsub  16762  gsumsubOLD  16763  telgsumfzslem  16805  telgsumfzs  16806  telgsums  16810  ablfacrp  16904  ablfac1lem  16906  ablfac1b  16908  ablfac1c  16909  ablfac1eulem  16910  ablfac1eu  16911  pgpfac1lem1  16912  pgpfac1lem2  16913  pgpfac1lem3a  16914  pgpfac1lem3  16915  pgpfac1lem4  16916  pgpfac1lem5  16917  pgpfac1  16918  pgpfaclem3  16921  pgpfac  16922  ablfaclem2  16924  ablfaclem3  16925  ablfac  16926  cnmsubglem  18245  zlmlmod  18324  frgpcyg  18376  dchrghm  23256  dchr1  23257  dchrinv  23261  dchr1re  23263  dchrpt  23267  dchrsum2  23268  sumdchr2  23270  dchrhash  23271  dchr2sum  23273  rpvmasumlem  23397  rpvmasum2  23422  dchrisum0re  23423  isnumbasgrplem1  30654  isnumbasabl  30659  isnumbasgrp  30660  dfacbasgrp  30661  dvalveclem  35822
  Copyright terms: Public domain W3C validator