Theorem ablgrp 19766

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

Syntax hints:   → wi 4   ∈ wcel 2108  Grpcgrp 18916  CMndccmn 19761  Abelcabl 19762

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 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-in 3933  df-abl 19764

This theorem is referenced by:  ablgrpd  19767  ablinvadd  19788  ablsub2inv  19789  ablsubadd  19790  ablsub4  19791  abladdsub4  19792  abladdsub  19793  ablsubadd23  19794  ablsubaddsub  19795  ablpncan2  19796  ablpncan3  19797  ablsubsub  19798  ablsubsub4  19799  ablpnpcan  19800  ablnncan  19801  ablnnncan  19803  ablnnncan1  19804  ablsubsub23  19805  mulgdi  19807  mulgghm  19809  mulgsubdi  19810  ghmabl  19813  invghm  19814  eqgabl  19815  odadd1  19829  odadd2  19830  odadd  19831  gexexlem  19833  gexex  19834  torsubg  19835  oddvdssubg  19836  prdsabld  19843  cnaddinv  19852  cyggexb  19880  gsumsub  19929  telgsumfzslem  19969  telgsumfzs  19970  telgsums  19974  ablfacrp  20049  ablfac1lem  20051  ablfac1b  20053  ablfac1c  20054  ablfac1eulem  20055  ablfac1eu  20056  pgpfac1lem1  20057  pgpfac1lem2  20058  pgpfac1lem3a  20059  pgpfac1lem3  20060  pgpfac1lem4  20061  pgpfac1lem5  20062  pgpfac1  20063  pgpfaclem3  20066  pgpfac  20067  ablfaclem2  20069  ablfaclem3  20070  ablfac  20071  rnglz  20125  rngpropd  20134  isringrng  20247  isrnghm  20401  isrnghmd  20411  idrnghm  20418  c0rnghm  20495  zrrnghm  20496  cnmsubglem  21398  zlmlmod  21483  frgpcyg  21534  efsubm  26512  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  33670  dvalveclem  41044  primrootscoprbij  42115  primrootspoweq0  42119  isnumbasgrplem1  43125  isnumbasabl  43130  isnumbasgrp  43131  dfacbasgrp  43132