Theorem ablgrp 19801

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

Syntax hints:   → wi 4   ∈ wcel 2136  Grpcgrp 18951  CMndccmn 19796  Abelcabl 19797

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1809  ax-4 1823  ax-5 1924  ax-6 1981  ax-7 2022  ax-8 2138  ax-9 2146  ax-ext 2728

This theorem depends on definitions:  df-bi 209  df-an 399  df-tru 1557  df-ex 1794  df-sb 2085  df-clab 2735  df-cleq 2748  df-clel 2831  df-v 3450  df-in 3906  df-abl 19799

This theorem is referenced by:  ablgrpd  19802  ablinvadd  19823  ablsub2inv  19824  ablsubadd  19825  ablsub4  19826  abladdsub4  19827  abladdsub  19828  ablsubadd23  19829  ablsubaddsub  19830  ablpncan2  19831  ablpncan3  19832  ablsubsub  19833  ablsubsub4  19834  ablpnpcan  19835  ablnncan  19836  ablnnncan  19838  ablnnncan1  19839  ablsubsub23  19840  mulgdi  19842  mulgghm  19844  mulgsubdi  19845  ghmabl  19848  invghm  19849  eqgabl  19850  odadd1  19864  odadd2  19865  odadd  19866  gexexlem  19868  gexex  19869  torsubg  19870  oddvdssubg  19871  prdsabld  19878  cnaddinv  19887  cyggexb  19915  gsumsub  19964  telgsumfzslem  20004  telgsumfzs  20005  telgsums  20009  ablfacrp  20084  ablfac1lem  20086  ablfac1b  20088  ablfac1c  20089  ablfac1eulem  20090  ablfac1eu  20091  pgpfac1lem1  20092  pgpfac1lem2  20093  pgpfac1lem3a  20094  pgpfac1lem3  20095  pgpfac1lem4  20096  pgpfac1lem5  20097  pgpfac1  20098  pgpfaclem3  20101  pgpfac  20102  ablfaclem2  20104  ablfaclem3  20105  ablfac  20106  rnglz  20187  rngpropd  20196  isringrng  20309  isrnghm  20462  isrnghmd  20472  idrnghm  20479  c0rnghm  20557  zrrnghm  20558  cnmsubglem  21455  zlmlmod  21547  frgpcyg  21598  efsubm  26586  dchrghm  27290  dchr1  27291  dchrinv  27295  dchr1re  27297  dchrpt  27301  dchrsum2  27302  sumdchr2  27304  dchrhash  27305  dchr2sum  27307  rpvmasumlem  27521  rpvmasum2  27546  dchrisum0re  27547  fedgmullem2  33881  dvalveclem  41597  primrootscoprbij  42667  primrootspoweq0  42671  isnumbasgrplem1  43626  isnumbasabl  43631  isnumbasgrp  43632  dfacbasgrp  43633