Theorem ablgrp 19861

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2142  Grpcgrp 19006  CMndccmn 19856  Abelcabl 19857

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-tru 1572  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-in 3911  df-abl 19859

This theorem is used by:  ablgrpd  19862  ablinvadd  19883  ablsub2inv  19884  ablsubadd  19885  ablsub4  19886  abladdsub4  19887  abladdsub  19888  ablsubadd23  19889  ablsubaddsub  19890  ablpncan2  19891  ablpncan3  19892  ablsubsub  19893  ablsubsub4  19894  ablpnpcan  19895  ablnncan  19896  ablnnncan  19898  ablnnncan1  19899  ablsubsub23  19900  mulgdi  19902  mulgghm  19904  mulgsubdi  19905  ghmabl  19908  invghm  19909  eqgabl  19910  odadd1  19924  odadd2  19925  odadd  19926  gexexlem  19928  gexex  19929  torsubg  19930  oddvdssubg  19931  prdsabld  19938  cnaddinv  19947  cyggexb  19975  gsumsub  20024  telgsumfzslem  20064  telgsumfzs  20065  telgsums  20069  ablfacrp  20144  ablfac1lem  20146  ablfac1b  20148  ablfac1c  20149  ablfac1eulem  20150  ablfac1eu  20151  pgpfac1lem1  20152  pgpfac1lem2  20153  pgpfac1lem3a  20154  pgpfac1lem3  20155  pgpfac1lem4  20156  pgpfac1lem5  20157  pgpfac1  20158  pgpfaclem3  20161  pgpfac  20162  ablfaclem2  20164  ablfaclem3  20165  ablfac  20166  rnglz  20249  rngpropd  20258  isringrng  20377  isrnghm  20530  isrnghmd  20540  idrnghm  20547  c0rnghm  20645  zrrnghm  20646  cnmsubglem  21591  zlmlmod  21683  frgpcyg  21734  efsubm  26727  dchrghm  27431  dchr1  27432  dchrinv  27436  dchr1re  27438  dchrpt  27442  dchrsum2  27443  sumdchr2  27445  dchrhash  27446  dchr2sum  27448  rpvmasumlem  27662  rpvmasum2  27687  dchrisum0re  27688  fedgmullem2  34029  dvalveclem  41827  primrootscoprbij  42897  primrootspoweq0  42901  isnumbasgrplem1  43856  isnumbasabl  43861  isnumbasgrp  43862  dfacbasgrp  43863