Theorem ablgrp 19760

Description: An Abelian group is a group. (Contributed by NM, 26-Aug-2011.)

Assertion

Ref	Expression
ablgrp	⊢ (𝐺 ∈ Abel → 𝐺 ∈ Grp)

Proof of Theorem ablgrp

Step	Hyp	Ref	Expression
1		isabl 19759	. 2 ⊢ (𝐺 ∈ Abel ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ CMnd))
2	1	simplbi 496	1 ⊢ (𝐺 ∈ Abel → 𝐺 ∈ Grp)

Syntax hints:   → wi 4   ∈ wcel 2114  Grpcgrp 18909  CMndccmn 19755  Abelcabl 19756

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-in 3897  df-abl 19758

This theorem is referenced by:  ablgrpd  19761  ablinvadd  19782  ablsub2inv  19783  ablsubadd  19784  ablsub4  19785  abladdsub4  19786  abladdsub  19787  ablsubadd23  19788  ablsubaddsub  19789  ablpncan2  19790  ablpncan3  19791  ablsubsub  19792  ablsubsub4  19793  ablpnpcan  19794  ablnncan  19795  ablnnncan  19797  ablnnncan1  19798  ablsubsub23  19799  mulgdi  19801  mulgghm  19803  mulgsubdi  19804  ghmabl  19807  invghm  19808  eqgabl  19809  odadd1  19823  odadd2  19824  odadd  19825  gexexlem  19827  gexex  19828  torsubg  19829  oddvdssubg  19830  prdsabld  19837  cnaddinv  19846  cyggexb  19874  gsumsub  19923  telgsumfzslem  19963  telgsumfzs  19964  telgsums  19968  ablfacrp  20043  ablfac1lem  20045  ablfac1b  20047  ablfac1c  20048  ablfac1eulem  20049  ablfac1eu  20050  pgpfac1lem1  20051  pgpfac1lem2  20052  pgpfac1lem3a  20053  pgpfac1lem3  20054  pgpfac1lem4  20055  pgpfac1lem5  20056  pgpfac1  20057  pgpfaclem3  20060  pgpfac  20061  ablfaclem2  20063  ablfaclem3  20064  ablfac  20065  rnglz  20146  rngpropd  20155  isringrng  20268  isrnghm  20421  isrnghmd  20431  idrnghm  20438  c0rnghm  20512  zrrnghm  20513  cnmsubglem  21410  zlmlmod  21502  frgpcyg  21553  efsubm  26515  dchrghm  27219  dchr1  27220  dchrinv  27224  dchr1re  27226  dchrpt  27230  dchrsum2  27231  sumdchr2  27233  dchrhash  27234  dchr2sum  27236  rpvmasumlem  27450  rpvmasum2  27475  dchrisum0re  27476  fedgmullem2  33774  dvalveclem  41471  primrootscoprbij  42541  primrootspoweq0  42545  isnumbasgrplem1  43529  isnumbasabl  43534  isnumbasgrp  43535  dfacbasgrp  43536