Theorem ablgrp 19758

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

Syntax hints:   → wi 4   ∈ wcel 2119  Grpcgrp 18907  CMndccmn 19753  Abelcabl 19754

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-v 3434  df-in 3897  df-abl 19756

This theorem is referenced by:  ablgrpd  19759  ablinvadd  19780  ablsub2inv  19781  ablsubadd  19782  ablsub4  19783  abladdsub4  19784  abladdsub  19785  ablsubadd23  19786  ablsubaddsub  19787  ablpncan2  19788  ablpncan3  19789  ablsubsub  19790  ablsubsub4  19791  ablpnpcan  19792  ablnncan  19793  ablnnncan  19795  ablnnncan1  19796  ablsubsub23  19797  mulgdi  19799  mulgghm  19801  mulgsubdi  19802  ghmabl  19805  invghm  19806  eqgabl  19807  odadd1  19821  odadd2  19822  odadd  19823  gexexlem  19825  gexex  19826  torsubg  19827  oddvdssubg  19828  prdsabld  19835  cnaddinv  19844  cyggexb  19872  gsumsub  19921  telgsumfzslem  19961  telgsumfzs  19962  telgsums  19966  ablfacrp  20041  ablfac1lem  20043  ablfac1b  20045  ablfac1c  20046  ablfac1eulem  20047  ablfac1eu  20048  pgpfac1lem1  20049  pgpfac1lem2  20050  pgpfac1lem3a  20051  pgpfac1lem3  20052  pgpfac1lem4  20053  pgpfac1lem5  20054  pgpfac1  20055  pgpfaclem3  20058  pgpfac  20059  ablfaclem2  20061  ablfaclem3  20062  ablfac  20063  rnglz  20144  rngpropd  20153  isringrng  20266  isrnghm  20419  isrnghmd  20429  idrnghm  20436  c0rnghm  20514  zrrnghm  20515  cnmsubglem  21412  zlmlmod  21504  frgpcyg  21555  efsubm  26540  dchrghm  27244  dchr1  27245  dchrinv  27249  dchr1re  27251  dchrpt  27255  dchrsum2  27256  sumdchr2  27258  dchrhash  27259  dchr2sum  27261  rpvmasumlem  27475  rpvmasum2  27500  dchrisum0re  27501  fedgmullem2  33821  dvalveclem  41518  primrootscoprbij  42588  primrootspoweq0  42592  isnumbasgrplem1  43547  isnumbasabl  43552  isnumbasgrp  43553  dfacbasgrp  43554