Theorem ablgrp 19306

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

Syntax hints:   → wi 4   ∈ wcel 2108  Grpcgrp 18492  CMndccmn 19301  Abelcabl 19302

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-abl 19304

This theorem is referenced by:  ablgrpd  19307  ablinvadd  19326  ablsub2inv  19327  ablsubadd  19328  ablsub4  19329  abladdsub4  19330  abladdsub  19331  ablpncan2  19332  ablpncan3  19333  ablsubsub  19334  ablsubsub4  19335  ablpnpcan  19336  ablnncan  19337  ablnnncan  19339  ablnnncan1  19340  ablsubsub23  19341  mulgdi  19343  mulgghm  19345  mulgsubdi  19346  ghmabl  19349  invghm  19350  eqgabl  19351  odadd1  19364  odadd2  19365  odadd  19366  gexexlem  19368  gexex  19369  torsubg  19370  oddvdssubg  19371  prdsabld  19378  cnaddinv  19387  cyggexb  19415  gsumsub  19464  telgsumfzslem  19504  telgsumfzs  19505  telgsums  19509  ablfacrp  19584  ablfac1lem  19586  ablfac1b  19588  ablfac1c  19589  ablfac1eulem  19590  ablfac1eu  19591  pgpfac1lem1  19592  pgpfac1lem2  19593  pgpfac1lem3a  19594  pgpfac1lem3  19595  pgpfac1lem4  19596  pgpfac1lem5  19597  pgpfac1  19598  pgpfaclem3  19601  pgpfac  19602  ablfaclem2  19604  ablfaclem3  19605  ablfac  19606  cnmsubglem  20573  zlmlmod  20640  frgpcyg  20693  efsubm  25612  dchrghm  26309  dchr1  26310  dchrinv  26314  dchr1re  26316  dchrpt  26320  dchrsum2  26321  sumdchr2  26323  dchrhash  26324  dchr2sum  26326  rpvmasumlem  26540  rpvmasum2  26565  dchrisum0re  26566  fedgmullem2  31613  dvalveclem  38966  isnumbasgrplem1  40842  isnumbasabl  40847  isnumbasgrp  40848  dfacbasgrp  40849  isringrng  45327  rnglz  45330  isrnghm  45338  isrnghmd  45348  idrnghm  45354  c0rnghm  45359  zrrnghm  45363