Theorem ablgrp 19722

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

Syntax hints:   → wi 4   ∈ wcel 2109  Grpcgrp 18872  CMndccmn 19717  Abelcabl 19718

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 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-in 3924  df-abl 19720

This theorem is referenced by:  ablgrpd  19723  ablinvadd  19744  ablsub2inv  19745  ablsubadd  19746  ablsub4  19747  abladdsub4  19748  abladdsub  19749  ablsubadd23  19750  ablsubaddsub  19751  ablpncan2  19752  ablpncan3  19753  ablsubsub  19754  ablsubsub4  19755  ablpnpcan  19756  ablnncan  19757  ablnnncan  19759  ablnnncan1  19760  ablsubsub23  19761  mulgdi  19763  mulgghm  19765  mulgsubdi  19766  ghmabl  19769  invghm  19770  eqgabl  19771  odadd1  19785  odadd2  19786  odadd  19787  gexexlem  19789  gexex  19790  torsubg  19791  oddvdssubg  19792  prdsabld  19799  cnaddinv  19808  cyggexb  19836  gsumsub  19885  telgsumfzslem  19925  telgsumfzs  19926  telgsums  19930  ablfacrp  20005  ablfac1lem  20007  ablfac1b  20009  ablfac1c  20010  ablfac1eulem  20011  ablfac1eu  20012  pgpfac1lem1  20013  pgpfac1lem2  20014  pgpfac1lem3a  20015  pgpfac1lem3  20016  pgpfac1lem4  20017  pgpfac1lem5  20018  pgpfac1  20019  pgpfaclem3  20022  pgpfac  20023  ablfaclem2  20025  ablfaclem3  20026  ablfac  20027  rnglz  20081  rngpropd  20090  isringrng  20203  isrnghm  20357  isrnghmd  20367  idrnghm  20374  c0rnghm  20451  zrrnghm  20452  cnmsubglem  21354  zlmlmod  21439  frgpcyg  21490  efsubm  26467  dchrghm  27174  dchr1  27175  dchrinv  27179  dchr1re  27181  dchrpt  27185  dchrsum2  27186  sumdchr2  27188  dchrhash  27189  dchr2sum  27191  rpvmasumlem  27405  rpvmasum2  27430  dchrisum0re  27431  fedgmullem2  33633  dvalveclem  41026  primrootscoprbij  42097  primrootspoweq0  42101  isnumbasgrplem1  43097  isnumbasabl  43102  isnumbasgrp  43103  dfacbasgrp  43104