Theorem ablgrp 19707

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

Syntax hints:   → wi 4   ∈ wcel 2113  Grpcgrp 18856  CMndccmn 19702  Abelcabl 19703

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-v 3440  df-in 3906  df-abl 19705

This theorem is referenced by:  ablgrpd  19708  ablinvadd  19729  ablsub2inv  19730  ablsubadd  19731  ablsub4  19732  abladdsub4  19733  abladdsub  19734  ablsubadd23  19735  ablsubaddsub  19736  ablpncan2  19737  ablpncan3  19738  ablsubsub  19739  ablsubsub4  19740  ablpnpcan  19741  ablnncan  19742  ablnnncan  19744  ablnnncan1  19745  ablsubsub23  19746  mulgdi  19748  mulgghm  19750  mulgsubdi  19751  ghmabl  19754  invghm  19755  eqgabl  19756  odadd1  19770  odadd2  19771  odadd  19772  gexexlem  19774  gexex  19775  torsubg  19776  oddvdssubg  19777  prdsabld  19784  cnaddinv  19793  cyggexb  19821  gsumsub  19870  telgsumfzslem  19910  telgsumfzs  19911  telgsums  19915  ablfacrp  19990  ablfac1lem  19992  ablfac1b  19994  ablfac1c  19995  ablfac1eulem  19996  ablfac1eu  19997  pgpfac1lem1  19998  pgpfac1lem2  19999  pgpfac1lem3a  20000  pgpfac1lem3  20001  pgpfac1lem4  20002  pgpfac1lem5  20003  pgpfac1  20004  pgpfaclem3  20007  pgpfac  20008  ablfaclem2  20010  ablfaclem3  20011  ablfac  20012  rnglz  20093  rngpropd  20102  isringrng  20215  isrnghm  20369  isrnghmd  20379  idrnghm  20386  c0rnghm  20460  zrrnghm  20461  cnmsubglem  21377  zlmlmod  21469  frgpcyg  21520  efsubm  26497  dchrghm  27204  dchr1  27205  dchrinv  27209  dchr1re  27211  dchrpt  27215  dchrsum2  27216  sumdchr2  27218  dchrhash  27219  dchr2sum  27221  rpvmasumlem  27435  rpvmasum2  27460  dchrisum0re  27461  fedgmullem2  33654  dvalveclem  41134  primrootscoprbij  42205  primrootspoweq0  42209  isnumbasgrplem1  43208  isnumbasabl  43213  isnumbasgrp  43214  dfacbasgrp  43215