Theorem ablgrp 19961

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  Grpcgrp 19106  CMndccmn 19956  Abelcabl 19957

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-in 3905  df-abl 19959

This theorem is used by:  ablgrpd  19962  ablinvadd  19983  ablsub2inv  19984  ablsubadd  19985  ablsub4  19986  abladdsub4  19987  abladdsub  19988  ablsubadd23  19989  ablsubaddsub  19990  ablpncan2  19991  ablpncan3  19992  ablsubsub  19993  ablsubsub4  19994  ablpnpcan  19995  ablnncan  19996  ablnnncan  19998  ablnnncan1  19999  ablsubsub23  20000  mulgdi  20002  mulgghm  20004  mulgsubdi  20005  ghmabl  20008  invghm  20009  eqgabl  20010  odadd1  20024  odadd2  20025  odadd  20026  gexexlem  20028  gexex  20029  torsubg  20030  oddvdssubg  20031  prdsabld  20038  cnaddinv  20047  cyggexb  20075  gsumsub  20124  telgsumfzslem  20164  telgsumfzs  20165  telgsums  20169  ablfacrp  20244  ablfac1lem  20246  ablfac1b  20248  ablfac1c  20249  ablfac1eulem  20250  ablfac1eu  20251  pgpfac1lem1  20252  pgpfac1lem2  20253  pgpfac1lem3a  20254  pgpfac1lem3  20255  pgpfac1lem4  20256  pgpfac1lem5  20257  pgpfac1  20258  pgpfaclem3  20261  pgpfac  20262  ablfaclem2  20264  ablfaclem3  20265  ablfac  20266  rnglz  20349  rngpropd  20358  isringrng  20478  dfring2  20479  isrnghm  20633  isrnghmd  20643  idrnghm  20650  c0rnghm  20749  zrrnghm  20750  cnmsubglem  21698  zlmlmod  21790  frgpcyg  21841  efsubm  26843  dchrghm  27547  dchr1  27548  dchrinv  27552  dchr1re  27554  dchrpt  27558  dchrsum2  27559  sumdchr2  27561  dchrhash  27562  dchr2sum  27564  rpvmasumlem  27778  rpvmasum2  27803  dchrisum0re  27804  fedgmullem2  34196  dvalveclem  42002  primrootscoprbij  43072  primrootspoweq0  43076  isnumbasgrplem1  44046  isnumbasabl  44051  isnumbasgrp  44052  dfacbasgrp  44053