Theorem ablgrp 19715

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

Syntax hints:   → wi 4   ∈ wcel 2109  Grpcgrp 18865  CMndccmn 19710  Abelcabl 19711

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-in 3921  df-abl 19713

This theorem is referenced by:  ablgrpd  19716  ablinvadd  19737  ablsub2inv  19738  ablsubadd  19739  ablsub4  19740  abladdsub4  19741  abladdsub  19742  ablsubadd23  19743  ablsubaddsub  19744  ablpncan2  19745  ablpncan3  19746  ablsubsub  19747  ablsubsub4  19748  ablpnpcan  19749  ablnncan  19750  ablnnncan  19752  ablnnncan1  19753  ablsubsub23  19754  mulgdi  19756  mulgghm  19758  mulgsubdi  19759  ghmabl  19762  invghm  19763  eqgabl  19764  odadd1  19778  odadd2  19779  odadd  19780  gexexlem  19782  gexex  19783  torsubg  19784  oddvdssubg  19785  prdsabld  19792  cnaddinv  19801  cyggexb  19829  gsumsub  19878  telgsumfzslem  19918  telgsumfzs  19919  telgsums  19923  ablfacrp  19998  ablfac1lem  20000  ablfac1b  20002  ablfac1c  20003  ablfac1eulem  20004  ablfac1eu  20005  pgpfac1lem1  20006  pgpfac1lem2  20007  pgpfac1lem3a  20008  pgpfac1lem3  20009  pgpfac1lem4  20010  pgpfac1lem5  20011  pgpfac1  20012  pgpfaclem3  20015  pgpfac  20016  ablfaclem2  20018  ablfaclem3  20019  ablfac  20020  rnglz  20074  rngpropd  20083  isringrng  20196  isrnghm  20350  isrnghmd  20360  idrnghm  20367  c0rnghm  20444  zrrnghm  20445  cnmsubglem  21347  zlmlmod  21432  frgpcyg  21483  efsubm  26460  dchrghm  27167  dchr1  27168  dchrinv  27172  dchr1re  27174  dchrpt  27178  dchrsum2  27179  sumdchr2  27181  dchrhash  27182  dchr2sum  27184  rpvmasumlem  27398  rpvmasum2  27423  dchrisum0re  27424  fedgmullem2  33626  dvalveclem  41019  primrootscoprbij  42090  primrootspoweq0  42094  isnumbasgrplem1  43090  isnumbasabl  43095  isnumbasgrp  43096  dfacbasgrp  43097