Theorem ablgrp 19749

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

Syntax hints:   → wi 4   ∈ wcel 2114  Grpcgrp 18898  CMndccmn 19744  Abelcabl 19745

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-in 3897  df-abl 19747

This theorem is referenced by:  ablgrpd  19750  ablinvadd  19771  ablsub2inv  19772  ablsubadd  19773  ablsub4  19774  abladdsub4  19775  abladdsub  19776  ablsubadd23  19777  ablsubaddsub  19778  ablpncan2  19779  ablpncan3  19780  ablsubsub  19781  ablsubsub4  19782  ablpnpcan  19783  ablnncan  19784  ablnnncan  19786  ablnnncan1  19787  ablsubsub23  19788  mulgdi  19790  mulgghm  19792  mulgsubdi  19793  ghmabl  19796  invghm  19797  eqgabl  19798  odadd1  19812  odadd2  19813  odadd  19814  gexexlem  19816  gexex  19817  torsubg  19818  oddvdssubg  19819  prdsabld  19826  cnaddinv  19835  cyggexb  19863  gsumsub  19912  telgsumfzslem  19952  telgsumfzs  19953  telgsums  19957  ablfacrp  20032  ablfac1lem  20034  ablfac1b  20036  ablfac1c  20037  ablfac1eulem  20038  ablfac1eu  20039  pgpfac1lem1  20040  pgpfac1lem2  20041  pgpfac1lem3a  20042  pgpfac1lem3  20043  pgpfac1lem4  20044  pgpfac1lem5  20045  pgpfac1  20046  pgpfaclem3  20049  pgpfac  20050  ablfaclem2  20052  ablfaclem3  20053  ablfac  20054  rnglz  20135  rngpropd  20144  isringrng  20257  isrnghm  20410  isrnghmd  20420  idrnghm  20427  c0rnghm  20501  zrrnghm  20502  cnmsubglem  21418  zlmlmod  21510  frgpcyg  21561  efsubm  26531  dchrghm  27238  dchr1  27239  dchrinv  27243  dchr1re  27245  dchrpt  27249  dchrsum2  27250  sumdchr2  27252  dchrhash  27253  dchr2sum  27255  rpvmasumlem  27469  rpvmasum2  27494  dchrisum0re  27495  fedgmullem2  33795  dvalveclem  41482  primrootscoprbij  42552  primrootspoweq0  42556  isnumbasgrplem1  43544  isnumbasabl  43549  isnumbasgrp  43550  dfacbasgrp  43551