Theorem ablgrp 19459

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

Syntax hints:   → wi 4   ∈ wcel 2105  Grpcgrp 18646  CMndccmn 19454  Abelcabl 19455

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2708

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3443  df-in 3904  df-abl 19457

This theorem is referenced by:  ablgrpd  19460  ablinvadd  19479  ablsub2inv  19480  ablsubadd  19481  ablsub4  19482  abladdsub4  19483  abladdsub  19484  ablpncan2  19485  ablpncan3  19486  ablsubsub  19487  ablsubsub4  19488  ablpnpcan  19489  ablnncan  19490  ablnnncan  19492  ablnnncan1  19493  ablsubsub23  19494  mulgdi  19496  mulgghm  19498  mulgsubdi  19499  ghmabl  19502  invghm  19503  eqgabl  19504  odadd1  19517  odadd2  19518  odadd  19519  gexexlem  19521  gexex  19522  torsubg  19523  oddvdssubg  19524  prdsabld  19531  cnaddinv  19540  cyggexb  19568  gsumsub  19617  telgsumfzslem  19657  telgsumfzs  19658  telgsums  19662  ablfacrp  19737  ablfac1lem  19739  ablfac1b  19741  ablfac1c  19742  ablfac1eulem  19743  ablfac1eu  19744  pgpfac1lem1  19745  pgpfac1lem2  19746  pgpfac1lem3a  19747  pgpfac1lem3  19748  pgpfac1lem4  19749  pgpfac1lem5  19750  pgpfac1  19751  pgpfaclem3  19754  pgpfac  19755  ablfaclem2  19757  ablfaclem3  19758  ablfac  19759  cnmsubglem  20733  zlmlmod  20800  frgpcyg  20853  efsubm  25779  dchrghm  26476  dchr1  26477  dchrinv  26481  dchr1re  26483  dchrpt  26487  dchrsum2  26488  sumdchr2  26490  dchrhash  26491  dchr2sum  26493  rpvmasumlem  26707  rpvmasum2  26732  dchrisum0re  26733  fedgmullem2  31817  dvalveclem  39244  isnumbasgrplem1  41130  isnumbasabl  41135  isnumbasgrp  41136  dfacbasgrp  41137  isringrng  45691  rnglz  45694  isrnghm  45702  isrnghmd  45712  idrnghm  45718  c0rnghm  45723  zrrnghm  45727