Theorem ablgrp 19690

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

Syntax hints:   → wi 4   ∈ wcel 2110  Grpcgrp 18838  CMndccmn 19685  Abelcabl 19686

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2112  ax-9 2120  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3436  df-in 3907  df-abl 19688

This theorem is referenced by:  ablgrpd  19691  ablinvadd  19712  ablsub2inv  19713  ablsubadd  19714  ablsub4  19715  abladdsub4  19716  abladdsub  19717  ablsubadd23  19718  ablsubaddsub  19719  ablpncan2  19720  ablpncan3  19721  ablsubsub  19722  ablsubsub4  19723  ablpnpcan  19724  ablnncan  19725  ablnnncan  19727  ablnnncan1  19728  ablsubsub23  19729  mulgdi  19731  mulgghm  19733  mulgsubdi  19734  ghmabl  19737  invghm  19738  eqgabl  19739  odadd1  19753  odadd2  19754  odadd  19755  gexexlem  19757  gexex  19758  torsubg  19759  oddvdssubg  19760  prdsabld  19767  cnaddinv  19776  cyggexb  19804  gsumsub  19853  telgsumfzslem  19893  telgsumfzs  19894  telgsums  19898  ablfacrp  19973  ablfac1lem  19975  ablfac1b  19977  ablfac1c  19978  ablfac1eulem  19979  ablfac1eu  19980  pgpfac1lem1  19981  pgpfac1lem2  19982  pgpfac1lem3a  19983  pgpfac1lem3  19984  pgpfac1lem4  19985  pgpfac1lem5  19986  pgpfac1  19987  pgpfaclem3  19990  pgpfac  19991  ablfaclem2  19993  ablfaclem3  19994  ablfac  19995  rnglz  20076  rngpropd  20085  isringrng  20198  isrnghm  20352  isrnghmd  20362  idrnghm  20369  c0rnghm  20443  zrrnghm  20444  cnmsubglem  21360  zlmlmod  21452  frgpcyg  21503  efsubm  26480  dchrghm  27187  dchr1  27188  dchrinv  27192  dchr1re  27194  dchrpt  27198  dchrsum2  27199  sumdchr2  27201  dchrhash  27202  dchr2sum  27204  rpvmasumlem  27418  rpvmasum2  27443  dchrisum0re  27444  fedgmullem2  33633  dvalveclem  41043  primrootscoprbij  42114  primrootspoweq0  42118  isnumbasgrplem1  43113  isnumbasabl  43118  isnumbasgrp  43119  dfacbasgrp  43120