Theorem ablgrp 19718

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

Syntax hints:   → wi 4   ∈ wcel 2114  Grpcgrp 18867  CMndccmn 19713  Abelcabl 19714

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 3443  df-in 3909  df-abl 19716

This theorem is referenced by:  ablgrpd  19719  ablinvadd  19740  ablsub2inv  19741  ablsubadd  19742  ablsub4  19743  abladdsub4  19744  abladdsub  19745  ablsubadd23  19746  ablsubaddsub  19747  ablpncan2  19748  ablpncan3  19749  ablsubsub  19750  ablsubsub4  19751  ablpnpcan  19752  ablnncan  19753  ablnnncan  19755  ablnnncan1  19756  ablsubsub23  19757  mulgdi  19759  mulgghm  19761  mulgsubdi  19762  ghmabl  19765  invghm  19766  eqgabl  19767  odadd1  19781  odadd2  19782  odadd  19783  gexexlem  19785  gexex  19786  torsubg  19787  oddvdssubg  19788  prdsabld  19795  cnaddinv  19804  cyggexb  19832  gsumsub  19881  telgsumfzslem  19921  telgsumfzs  19922  telgsums  19926  ablfacrp  20001  ablfac1lem  20003  ablfac1b  20005  ablfac1c  20006  ablfac1eulem  20007  ablfac1eu  20008  pgpfac1lem1  20009  pgpfac1lem2  20010  pgpfac1lem3a  20011  pgpfac1lem3  20012  pgpfac1lem4  20013  pgpfac1lem5  20014  pgpfac1  20015  pgpfaclem3  20018  pgpfac  20019  ablfaclem2  20021  ablfaclem3  20022  ablfac  20023  rnglz  20104  rngpropd  20113  isringrng  20226  isrnghm  20381  isrnghmd  20391  idrnghm  20398  c0rnghm  20472  zrrnghm  20473  cnmsubglem  21389  zlmlmod  21481  frgpcyg  21532  efsubm  26520  dchrghm  27227  dchr1  27228  dchrinv  27232  dchr1re  27234  dchrpt  27238  dchrsum2  27239  sumdchr2  27241  dchrhash  27242  dchr2sum  27244  rpvmasumlem  27458  rpvmasum2  27483  dchrisum0re  27484  fedgmullem2  33768  dvalveclem  41322  primrootscoprbij  42393  primrootspoweq0  42397  isnumbasgrplem1  43379  isnumbasabl  43384  isnumbasgrp  43385  dfacbasgrp  43386