Theorem ablgrp 19703

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

Syntax hints:   → wi 4   ∈ wcel 2111  Grpcgrp 18852  CMndccmn 19698  Abelcabl 19699

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 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-in 3904  df-abl 19701

This theorem is referenced by:  ablgrpd  19704  ablinvadd  19725  ablsub2inv  19726  ablsubadd  19727  ablsub4  19728  abladdsub4  19729  abladdsub  19730  ablsubadd23  19731  ablsubaddsub  19732  ablpncan2  19733  ablpncan3  19734  ablsubsub  19735  ablsubsub4  19736  ablpnpcan  19737  ablnncan  19738  ablnnncan  19740  ablnnncan1  19741  ablsubsub23  19742  mulgdi  19744  mulgghm  19746  mulgsubdi  19747  ghmabl  19750  invghm  19751  eqgabl  19752  odadd1  19766  odadd2  19767  odadd  19768  gexexlem  19770  gexex  19771  torsubg  19772  oddvdssubg  19773  prdsabld  19780  cnaddinv  19789  cyggexb  19817  gsumsub  19866  telgsumfzslem  19906  telgsumfzs  19907  telgsums  19911  ablfacrp  19986  ablfac1lem  19988  ablfac1b  19990  ablfac1c  19991  ablfac1eulem  19992  ablfac1eu  19993  pgpfac1lem1  19994  pgpfac1lem2  19995  pgpfac1lem3a  19996  pgpfac1lem3  19997  pgpfac1lem4  19998  pgpfac1lem5  19999  pgpfac1  20000  pgpfaclem3  20003  pgpfac  20004  ablfaclem2  20006  ablfaclem3  20007  ablfac  20008  rnglz  20089  rngpropd  20098  isringrng  20211  isrnghm  20365  isrnghmd  20375  idrnghm  20382  c0rnghm  20456  zrrnghm  20457  cnmsubglem  21373  zlmlmod  21465  frgpcyg  21516  efsubm  26493  dchrghm  27200  dchr1  27201  dchrinv  27205  dchr1re  27207  dchrpt  27211  dchrsum2  27212  sumdchr2  27214  dchrhash  27215  dchr2sum  27217  rpvmasumlem  27431  rpvmasum2  27456  dchrisum0re  27457  fedgmullem2  33650  dvalveclem  41130  primrootscoprbij  42201  primrootspoweq0  42205  isnumbasgrplem1  43199  isnumbasabl  43204  isnumbasgrp  43205  dfacbasgrp  43206