Theorem ablgrp 19682

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

Syntax hints:   → wi 4   ∈ wcel 2109  Grpcgrp 18830  CMndccmn 19677  Abelcabl 19678

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 3440  df-in 3912  df-abl 19680

This theorem is referenced by:  ablgrpd  19683  ablinvadd  19704  ablsub2inv  19705  ablsubadd  19706  ablsub4  19707  abladdsub4  19708  abladdsub  19709  ablsubadd23  19710  ablsubaddsub  19711  ablpncan2  19712  ablpncan3  19713  ablsubsub  19714  ablsubsub4  19715  ablpnpcan  19716  ablnncan  19717  ablnnncan  19719  ablnnncan1  19720  ablsubsub23  19721  mulgdi  19723  mulgghm  19725  mulgsubdi  19726  ghmabl  19729  invghm  19730  eqgabl  19731  odadd1  19745  odadd2  19746  odadd  19747  gexexlem  19749  gexex  19750  torsubg  19751  oddvdssubg  19752  prdsabld  19759  cnaddinv  19768  cyggexb  19796  gsumsub  19845  telgsumfzslem  19885  telgsumfzs  19886  telgsums  19890  ablfacrp  19965  ablfac1lem  19967  ablfac1b  19969  ablfac1c  19970  ablfac1eulem  19971  ablfac1eu  19972  pgpfac1lem1  19973  pgpfac1lem2  19974  pgpfac1lem3a  19975  pgpfac1lem3  19976  pgpfac1lem4  19977  pgpfac1lem5  19978  pgpfac1  19979  pgpfaclem3  19982  pgpfac  19983  ablfaclem2  19985  ablfaclem3  19986  ablfac  19987  rnglz  20068  rngpropd  20077  isringrng  20190  isrnghm  20344  isrnghmd  20354  idrnghm  20361  c0rnghm  20438  zrrnghm  20439  cnmsubglem  21355  zlmlmod  21447  frgpcyg  21498  efsubm  26476  dchrghm  27183  dchr1  27184  dchrinv  27188  dchr1re  27190  dchrpt  27194  dchrsum2  27195  sumdchr2  27197  dchrhash  27198  dchr2sum  27200  rpvmasumlem  27414  rpvmasum2  27439  dchrisum0re  27440  fedgmullem2  33602  dvalveclem  41004  primrootscoprbij  42075  primrootspoweq0  42079  isnumbasgrplem1  43074  isnumbasabl  43079  isnumbasgrp  43080  dfacbasgrp  43081