Theorem ablgrp 19400

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

Syntax hints:   → wi 4   ∈ wcel 2107  Grpcgrp 18586  CMndccmn 19395  Abelcabl 19396

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 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3435  df-in 3895  df-abl 19398

This theorem is referenced by:  ablgrpd  19401  ablinvadd  19420  ablsub2inv  19421  ablsubadd  19422  ablsub4  19423  abladdsub4  19424  abladdsub  19425  ablpncan2  19426  ablpncan3  19427  ablsubsub  19428  ablsubsub4  19429  ablpnpcan  19430  ablnncan  19431  ablnnncan  19433  ablnnncan1  19434  ablsubsub23  19435  mulgdi  19437  mulgghm  19439  mulgsubdi  19440  ghmabl  19443  invghm  19444  eqgabl  19445  odadd1  19458  odadd2  19459  odadd  19460  gexexlem  19462  gexex  19463  torsubg  19464  oddvdssubg  19465  prdsabld  19472  cnaddinv  19481  cyggexb  19509  gsumsub  19558  telgsumfzslem  19598  telgsumfzs  19599  telgsums  19603  ablfacrp  19678  ablfac1lem  19680  ablfac1b  19682  ablfac1c  19683  ablfac1eulem  19684  ablfac1eu  19685  pgpfac1lem1  19686  pgpfac1lem2  19687  pgpfac1lem3a  19688  pgpfac1lem3  19689  pgpfac1lem4  19690  pgpfac1lem5  19691  pgpfac1  19692  pgpfaclem3  19695  pgpfac  19696  ablfaclem2  19698  ablfaclem3  19699  ablfac  19700  cnmsubglem  20670  zlmlmod  20737  frgpcyg  20790  efsubm  25716  dchrghm  26413  dchr1  26414  dchrinv  26418  dchr1re  26420  dchrpt  26424  dchrsum2  26425  sumdchr2  26427  dchrhash  26428  dchr2sum  26430  rpvmasumlem  26644  rpvmasum2  26669  dchrisum0re  26670  fedgmullem2  31720  dvalveclem  39046  isnumbasgrplem1  40933  isnumbasabl  40938  isnumbasgrp  40939  dfacbasgrp  40940  isringrng  45450  rnglz  45453  isrnghm  45461  isrnghmd  45471  idrnghm  45477  c0rnghm  45482  zrrnghm  45486