Theorem ablgrp 19846

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

Syntax hints:   → wi 4   ∈ wcel 2145  Grpcgrp 18990  CMndccmn 19841  Abelcabl 19842

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-in 3914  df-abl 19844

This theorem is referenced by:  ablgrpd  19847  ablinvadd  19868  ablsub2inv  19869  ablsubadd  19870  ablsub4  19871  abladdsub4  19872  abladdsub  19873  ablsubadd23  19874  ablsubaddsub  19875  ablpncan2  19876  ablpncan3  19877  ablsubsub  19878  ablsubsub4  19879  ablpnpcan  19880  ablnncan  19881  ablnnncan  19883  ablnnncan1  19884  ablsubsub23  19885  mulgdi  19887  mulgghm  19889  mulgsubdi  19890  ghmabl  19893  invghm  19894  eqgabl  19895  odadd1  19909  odadd2  19910  odadd  19911  gexexlem  19913  gexex  19914  torsubg  19915  oddvdssubg  19916  prdsabld  19923  cnaddinv  19932  cyggexb  19960  gsumsub  20009  telgsumfzslem  20049  telgsumfzs  20050  telgsums  20054  ablfacrp  20129  ablfac1lem  20131  ablfac1b  20133  ablfac1c  20134  ablfac1eulem  20135  ablfac1eu  20136  pgpfac1lem1  20137  pgpfac1lem2  20138  pgpfac1lem3a  20139  pgpfac1lem3  20140  pgpfac1lem4  20141  pgpfac1lem5  20142  pgpfac1  20143  pgpfaclem3  20146  pgpfac  20147  ablfaclem2  20149  ablfaclem3  20150  ablfac  20151  rnglz  20234  rngpropd  20243  isringrng  20361  isrnghm  20514  isrnghmd  20524  idrnghm  20531  c0rnghm  20611  zrrnghm  20612  cnmsubglem  21540  zlmlmod  21632  frgpcyg  21683  efsubm  26674  dchrghm  27378  dchr1  27379  dchrinv  27383  dchr1re  27385  dchrpt  27389  dchrsum2  27390  sumdchr2  27392  dchrhash  27393  dchr2sum  27395  rpvmasumlem  27609  rpvmasum2  27634  dchrisum0re  27635  fedgmullem2  33937  dvalveclem  41661  primrootscoprbij  42731  primrootspoweq0  42735  isnumbasgrplem1  43690  isnumbasabl  43695  isnumbasgrp  43696  dfacbasgrp  43697