Theorem ablgrp 19803

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 19802	. 2 ⊢ (𝐺 ∈ Abel ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ CMnd))
2	1	simplbi 497	1 ⊢ (𝐺 ∈ Abel → 𝐺 ∈ Grp)

Syntax hints:   → wi 4   ∈ wcel 2108  Grpcgrp 18951  CMndccmn 19798  Abelcabl 19799

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-in 3958  df-abl 19801

This theorem is referenced by:  ablgrpd  19804  ablinvadd  19825  ablsub2inv  19826  ablsubadd  19827  ablsub4  19828  abladdsub4  19829  abladdsub  19830  ablsubadd23  19831  ablsubaddsub  19832  ablpncan2  19833  ablpncan3  19834  ablsubsub  19835  ablsubsub4  19836  ablpnpcan  19837  ablnncan  19838  ablnnncan  19840  ablnnncan1  19841  ablsubsub23  19842  mulgdi  19844  mulgghm  19846  mulgsubdi  19847  ghmabl  19850  invghm  19851  eqgabl  19852  odadd1  19866  odadd2  19867  odadd  19868  gexexlem  19870  gexex  19871  torsubg  19872  oddvdssubg  19873  prdsabld  19880  cnaddinv  19889  cyggexb  19917  gsumsub  19966  telgsumfzslem  20006  telgsumfzs  20007  telgsums  20011  ablfacrp  20086  ablfac1lem  20088  ablfac1b  20090  ablfac1c  20091  ablfac1eulem  20092  ablfac1eu  20093  pgpfac1lem1  20094  pgpfac1lem2  20095  pgpfac1lem3a  20096  pgpfac1lem3  20097  pgpfac1lem4  20098  pgpfac1lem5  20099  pgpfac1  20100  pgpfaclem3  20103  pgpfac  20104  ablfaclem2  20106  ablfaclem3  20107  ablfac  20108  rnglz  20162  rngpropd  20171  isringrng  20284  isrnghm  20441  isrnghmd  20451  idrnghm  20458  c0rnghm  20535  zrrnghm  20536  cnmsubglem  21448  zlmlmod  21537  frgpcyg  21592  efsubm  26593  dchrghm  27300  dchr1  27301  dchrinv  27305  dchr1re  27307  dchrpt  27311  dchrsum2  27312  sumdchr2  27314  dchrhash  27315  dchr2sum  27317  rpvmasumlem  27531  rpvmasum2  27556  dchrisum0re  27557  fedgmullem2  33681  dvalveclem  41027  primrootscoprbij  42103  primrootspoweq0  42107  isnumbasgrplem1  43113  isnumbasabl  43118  isnumbasgrp  43119  dfacbasgrp  43120