Theorem ablgrp 20000

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  Grpcgrp 19145  CMndccmn 19995  Abelcabl 19996

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-in 4091  df-abl 19998

This theorem is used by:  ablgrpd  20001  ablinvadd  20022  ablsub2inv  20023  ablsubadd  20024  ablsub4  20025  abladdsub4  20026  abladdsub  20027  ablsubadd23  20028  ablsubaddsub  20029  ablpncan2  20030  ablpncan3  20031  ablsubsub  20032  ablsubsub4  20033  ablpnpcan  20034  ablnncan  20035  ablnnncan  20037  ablnnncan1  20038  ablsubsub23  20039  mulgdi  20041  mulgghm  20043  mulgsubdi  20044  ghmabl  20047  invghm  20048  eqgabl  20049  odadd1  20063  odadd2  20064  odadd  20065  gexexlem  20067  gexex  20068  torsubg  20069  oddvdssubg  20070  prdsabld  20077  cnaddinv  20086  cyggexb  20114  gsumsub  20163  telgsumfzslem  20203  telgsumfzs  20204  telgsums  20208  ablfacrp  20283  ablfac1lem  20285  ablfac1b  20287  ablfac1c  20288  ablfac1eulem  20289  ablfac1eu  20290  pgpfac1lem1  20291  pgpfac1lem2  20292  pgpfac1lem3a  20293  pgpfac1lem3  20294  pgpfac1lem4  20295  pgpfac1lem5  20296  pgpfac1  20297  pgpfaclem3  20300  pgpfac  20301  ablfaclem2  20303  ablfaclem3  20304  ablfac  20305  rnglz  20388  rngpropd  20397  isringrng  20517  dfring2  20518  isrnghm  20672  isrnghmd  20682  idrnghm  20689  c0rnghm  20788  zrrnghm  20789  cnmsubglem  21737  zlmlmod  21829  frgpcyg  21880  efsubm  26880  dchrghm  27584  dchr1  27585  dchrinv  27589  dchr1re  27591  dchrpt  27595  dchrsum2  27596  sumdchr2  27598  dchrhash  27599  dchr2sum  27601  rpvmasumlem  27815  rpvmasum2  27840  dchrisum0re  27841  fedgmullem2  34305  dvalveclem  42158  primrootscoprbij  43228  primrootspoweq0  43232  isnumbasgrplem1  44179  isnumbasabl  44184  isnumbasgrp  44185  dfacbasgrp  44186