Theorem ablgrp 18021

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

Syntax hints:   → wi 4   ∈ wcel 1977  Grpcgrp 17245  CMndccmn 18016  Abelcabl 18017

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-in 3547  df-abl 18019

This theorem is referenced by:  ablinvadd  18038  ablsub2inv  18039  ablsubadd  18040  ablsub4  18041  abladdsub4  18042  abladdsub  18043  ablpncan2  18044  ablpncan3  18045  ablsubsub  18046  ablsubsub4  18047  ablpnpcan  18048  ablnncan  18049  ablnnncan  18051  ablnnncan1  18052  ablsubsub23  18053  mulgdi  18055  mulgghm  18057  mulgsubdi  18058  ghmabl  18061  invghm  18062  eqgabl  18063  odadd1  18074  odadd2  18075  odadd  18076  gexexlem  18078  gexex  18079  torsubg  18080  oddvdssubg  18081  prdsabld  18088  cnaddinv  18097  cyggexb  18123  gsumsub  18171  telgsumfzslem  18208  telgsumfzs  18209  telgsums  18213  ablfacrp  18288  ablfac1lem  18290  ablfac1b  18292  ablfac1c  18293  ablfac1eulem  18294  ablfac1eu  18295  pgpfac1lem1  18296  pgpfac1lem2  18297  pgpfac1lem3a  18298  pgpfac1lem3  18299  pgpfac1lem4  18300  pgpfac1lem5  18301  pgpfac1  18302  pgpfaclem3  18305  pgpfac  18306  ablfaclem2  18308  ablfaclem3  18309  ablfac  18310  cnmsubglem  19628  zlmlmod  19690  frgpcyg  19741  efsubm  24101  dchrghm  24781  dchr1  24782  dchrinv  24786  dchr1re  24788  dchrpt  24792  dchrsum2  24793  sumdchr2  24795  dchrhash  24796  dchr2sum  24798  rpvmasumlem  24976  rpvmasum2  25001  dchrisum0re  25002  dvalveclem  35332  isnumbasgrplem1  36690  isnumbasabl  36695  isnumbasgrp  36696  dfacbasgrp  36697  isringrng  41671  rnglz  41674  isrnghm  41682  isrnghmd  41692  idrnghm  41698  c0rnghm  41703  zrrnghm  41707