Theorem ablgrp 19653

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

Syntax hints:   → wi 4   ∈ wcel 2107  Grpcgrp 18819  CMndccmn 19648  Abelcabl 19649

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-abl 19651

This theorem is referenced by:  ablgrpd  19654  ablinvadd  19675  ablsub2inv  19676  ablsubadd  19677  ablsub4  19678  abladdsub4  19679  abladdsub  19680  ablsubadd23  19681  ablsubaddsub  19682  ablpncan2  19683  ablpncan3  19684  ablsubsub  19685  ablsubsub4  19686  ablpnpcan  19687  ablnncan  19688  ablnnncan  19690  ablnnncan1  19691  ablsubsub23  19692  mulgdi  19694  mulgghm  19696  mulgsubdi  19697  ghmabl  19700  invghm  19701  eqgabl  19702  odadd1  19716  odadd2  19717  odadd  19718  gexexlem  19720  gexex  19721  torsubg  19722  oddvdssubg  19723  prdsabld  19730  cnaddinv  19739  cyggexb  19767  gsumsub  19816  telgsumfzslem  19856  telgsumfzs  19857  telgsums  19861  ablfacrp  19936  ablfac1lem  19938  ablfac1b  19940  ablfac1c  19941  ablfac1eulem  19942  ablfac1eu  19943  pgpfac1lem1  19944  pgpfac1lem2  19945  pgpfac1lem3a  19946  pgpfac1lem3  19947  pgpfac1lem4  19948  pgpfac1lem5  19949  pgpfac1  19950  pgpfaclem3  19953  pgpfac  19954  ablfaclem2  19956  ablfaclem3  19957  ablfac  19958  cnmsubglem  21008  zlmlmod  21076  frgpcyg  21129  efsubm  26060  dchrghm  26759  dchr1  26760  dchrinv  26764  dchr1re  26766  dchrpt  26770  dchrsum2  26771  sumdchr2  26773  dchrhash  26774  dchr2sum  26776  rpvmasumlem  26990  rpvmasum2  27015  dchrisum0re  27016  fedgmullem2  32746  dvalveclem  39944  isnumbasgrplem1  41891  isnumbasabl  41896  isnumbasgrp  41897  dfacbasgrp  41898  isringrng  46705  rnglz  46712  rngpropd  46721  isrnghm  46738  isrnghmd  46748  idrnghm  46755  c0rnghm  46760  zrrnghm  46764