Theorem ablgrp 20029

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  Grpcgrp 19173  CMndccmn 20024  Abelcabl 20025

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-in 4094  df-abl 20027

This theorem is used by:  ablgrpd  20030  ablinvadd  20051  ablsub2inv  20052  ablsubadd  20053  ablsub4  20054  abladdsub4  20055  abladdsub  20056  ablsubadd23  20057  ablsubaddsub  20058  ablpncan2  20059  ablpncan3  20060  ablsubsub  20061  ablsubsub4  20062  ablpnpcan  20063  ablnncan  20064  ablnnncan  20066  ablnnncan1  20067  ablsubsub23  20068  mulgdi  20070  mulgghm  20072  mulgsubdi  20073  ghmabl  20076  invghm  20077  eqgabl  20078  odadd1  20092  odadd2  20093  odadd  20094  gexexlem  20096  gexex  20097  torsubg  20098  oddvdssubg  20099  prdsabld  20106  cnaddinv  20115  cyggexb  20143  gsumsub  20192  telgsumfzslem  20232  telgsumfzs  20233  telgsums  20237  ablfacrp  20312  ablfac1lem  20314  ablfac1b  20316  ablfac1c  20317  ablfac1eulem  20318  ablfac1eu  20319  pgpfac1lem1  20320  pgpfac1lem2  20321  pgpfac1lem3a  20322  pgpfac1lem3  20323  pgpfac1lem4  20324  pgpfac1lem5  20325  pgpfac1  20326  pgpfaclem3  20329  pgpfac  20330  ablfaclem2  20332  ablfaclem3  20333  ablfac  20334  rnglz  20417  rngpropd  20426  isringrng  20546  dfring2  20547  isrnghm  20701  isrnghmd  20711  idrnghm  20718  c0rnghm  20817  zrrnghm  20818  cnmsubglem  21766  zlmlmod  21858  frgpcyg  21909  efsubm  26909  dchrghm  27613  dchr1  27614  dchrinv  27618  dchr1re  27620  dchrpt  27624  dchrsum2  27625  sumdchr2  27627  dchrhash  27628  dchr2sum  27630  rpvmasumlem  27844  rpvmasum2  27869  dchrisum0re  27870  fedgmullem2  34332  dvalveclem  42274  primrootscoprbij  43344  primrootspoweq0  43348  isnumbasgrplem1  44295  isnumbasabl  44300  isnumbasgrp  44301  dfacbasgrp  44302