Theorem ablgrp 19854

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

Syntax hints:   → wi 4   ∈ wcel 2141  Grpcgrp 18999  CMndccmn 19849  Abelcabl 19850

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1571  df-ex 1808  df-sb 2095  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-in 3911  df-abl 19852

This theorem is referenced by:  ablgrpd  19855  ablinvadd  19876  ablsub2inv  19877  ablsubadd  19878  ablsub4  19879  abladdsub4  19880  abladdsub  19881  ablsubadd23  19882  ablsubaddsub  19883  ablpncan2  19884  ablpncan3  19885  ablsubsub  19886  ablsubsub4  19887  ablpnpcan  19888  ablnncan  19889  ablnnncan  19891  ablnnncan1  19892  ablsubsub23  19893  mulgdi  19895  mulgghm  19897  mulgsubdi  19898  ghmabl  19901  invghm  19902  eqgabl  19903  odadd1  19917  odadd2  19918  odadd  19919  gexexlem  19921  gexex  19922  torsubg  19923  oddvdssubg  19924  prdsabld  19931  cnaddinv  19940  cyggexb  19968  gsumsub  20017  telgsumfzslem  20057  telgsumfzs  20058  telgsums  20062  ablfacrp  20137  ablfac1lem  20139  ablfac1b  20141  ablfac1c  20142  ablfac1eulem  20143  ablfac1eu  20144  pgpfac1lem1  20145  pgpfac1lem2  20146  pgpfac1lem3a  20147  pgpfac1lem3  20148  pgpfac1lem4  20149  pgpfac1lem5  20150  pgpfac1  20151  pgpfaclem3  20154  pgpfac  20155  ablfaclem2  20157  ablfaclem3  20158  ablfac  20159  rnglz  20242  rngpropd  20251  isringrng  20369  isrnghm  20522  isrnghmd  20532  idrnghm  20539  c0rnghm  20619  zrrnghm  20620  cnmsubglem  21559  zlmlmod  21651  frgpcyg  21702  efsubm  26692  dchrghm  27396  dchr1  27397  dchrinv  27401  dchr1re  27403  dchrpt  27407  dchrsum2  27408  sumdchr2  27410  dchrhash  27411  dchr2sum  27413  rpvmasumlem  27627  rpvmasum2  27652  dchrisum0re  27653  fedgmullem2  33986  dvalveclem  41767  primrootscoprbij  42837  primrootspoweq0  42841  isnumbasgrplem1  43798  isnumbasabl  43803  isnumbasgrp  43804  dfacbasgrp  43805