Theorem ablgrp 19726

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

Syntax hints:   → wi 4   ∈ wcel 2114  Grpcgrp 18875  CMndccmn 19721  Abelcabl 19722

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 3444  df-in 3910  df-abl 19724

This theorem is referenced by:  ablgrpd  19727  ablinvadd  19748  ablsub2inv  19749  ablsubadd  19750  ablsub4  19751  abladdsub4  19752  abladdsub  19753  ablsubadd23  19754  ablsubaddsub  19755  ablpncan2  19756  ablpncan3  19757  ablsubsub  19758  ablsubsub4  19759  ablpnpcan  19760  ablnncan  19761  ablnnncan  19763  ablnnncan1  19764  ablsubsub23  19765  mulgdi  19767  mulgghm  19769  mulgsubdi  19770  ghmabl  19773  invghm  19774  eqgabl  19775  odadd1  19789  odadd2  19790  odadd  19791  gexexlem  19793  gexex  19794  torsubg  19795  oddvdssubg  19796  prdsabld  19803  cnaddinv  19812  cyggexb  19840  gsumsub  19889  telgsumfzslem  19929  telgsumfzs  19930  telgsums  19934  ablfacrp  20009  ablfac1lem  20011  ablfac1b  20013  ablfac1c  20014  ablfac1eulem  20015  ablfac1eu  20016  pgpfac1lem1  20017  pgpfac1lem2  20018  pgpfac1lem3a  20019  pgpfac1lem3  20020  pgpfac1lem4  20021  pgpfac1lem5  20022  pgpfac1  20023  pgpfaclem3  20026  pgpfac  20027  ablfaclem2  20029  ablfaclem3  20030  ablfac  20031  rnglz  20112  rngpropd  20121  isringrng  20234  isrnghm  20389  isrnghmd  20399  idrnghm  20406  c0rnghm  20480  zrrnghm  20481  cnmsubglem  21397  zlmlmod  21489  frgpcyg  21540  efsubm  26528  dchrghm  27235  dchr1  27236  dchrinv  27240  dchr1re  27242  dchrpt  27246  dchrsum2  27247  sumdchr2  27249  dchrhash  27250  dchr2sum  27252  rpvmasumlem  27466  rpvmasum2  27491  dchrisum0re  27492  fedgmullem2  33807  dvalveclem  41390  primrootscoprbij  42461  primrootspoweq0  42465  isnumbasgrplem1  43447  isnumbasabl  43452  isnumbasgrp  43453  dfacbasgrp  43454