Theorem ablgrp 19785

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

Syntax hints:   → wi 4   ∈ wcel 2099  Grpcgrp 18930  CMndccmn 19780  Abelcabl 19781

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-v 3464  df-in 3954  df-abl 19783

This theorem is referenced by:  ablgrpd  19786  ablinvadd  19807  ablsub2inv  19808  ablsubadd  19809  ablsub4  19810  abladdsub4  19811  abladdsub  19812  ablsubadd23  19813  ablsubaddsub  19814  ablpncan2  19815  ablpncan3  19816  ablsubsub  19817  ablsubsub4  19818  ablpnpcan  19819  ablnncan  19820  ablnnncan  19822  ablnnncan1  19823  ablsubsub23  19824  mulgdi  19826  mulgghm  19828  mulgsubdi  19829  ghmabl  19832  invghm  19833  eqgabl  19834  odadd1  19848  odadd2  19849  odadd  19850  gexexlem  19852  gexex  19853  torsubg  19854  oddvdssubg  19855  prdsabld  19862  cnaddinv  19871  cyggexb  19899  gsumsub  19948  telgsumfzslem  19988  telgsumfzs  19989  telgsums  19993  ablfacrp  20068  ablfac1lem  20070  ablfac1b  20072  ablfac1c  20073  ablfac1eulem  20074  ablfac1eu  20075  pgpfac1lem1  20076  pgpfac1lem2  20077  pgpfac1lem3a  20078  pgpfac1lem3  20079  pgpfac1lem4  20080  pgpfac1lem5  20081  pgpfac1  20082  pgpfaclem3  20085  pgpfac  20086  ablfaclem2  20088  ablfaclem3  20089  ablfac  20090  rnglz  20150  rngpropd  20159  isringrng  20268  isrnghm  20425  isrnghmd  20435  idrnghm  20442  c0rnghm  20519  zrrnghm  20520  cnmsubglem  21429  zlmlmod  21518  frgpcyg  21573  efsubm  26581  dchrghm  27288  dchr1  27289  dchrinv  27293  dchr1re  27295  dchrpt  27299  dchrsum2  27300  sumdchr2  27302  dchrhash  27303  dchr2sum  27305  rpvmasumlem  27519  rpvmasum2  27544  dchrisum0re  27545  fedgmullem2  33527  dvalveclem  40726  primrootscoprbij  41802  primrootspoweq0  41806  isnumbasgrplem1  42780  isnumbasabl  42785  isnumbasgrp  42786  dfacbasgrp  42787