Theorem ablgrp 18910

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

Syntax hints:   → wi 4   ∈ wcel 2110  Grpcgrp 18102  CMndccmn 18905  Abelcabl 18906

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-in 3942  df-abl 18908

This theorem is referenced by:  ablgrpd  18911  ablinvadd  18929  ablsub2inv  18930  ablsubadd  18931  ablsub4  18932  abladdsub4  18933  abladdsub  18934  ablpncan2  18935  ablpncan3  18936  ablsubsub  18937  ablsubsub4  18938  ablpnpcan  18939  ablnncan  18940  ablnnncan  18942  ablnnncan1  18943  ablsubsub23  18944  mulgdi  18946  mulgghm  18948  mulgsubdi  18949  ghmabl  18952  invghm  18953  eqgabl  18954  odadd1  18967  odadd2  18968  odadd  18969  gexexlem  18971  gexex  18972  torsubg  18973  oddvdssubg  18974  prdsabld  18981  cnaddinv  18990  cyggexb  19018  gsumsub  19067  telgsumfzslem  19107  telgsumfzs  19108  telgsums  19112  ablfacrp  19187  ablfac1lem  19189  ablfac1b  19191  ablfac1c  19192  ablfac1eulem  19193  ablfac1eu  19194  pgpfac1lem1  19195  pgpfac1lem2  19196  pgpfac1lem3a  19197  pgpfac1lem3  19198  pgpfac1lem4  19199  pgpfac1lem5  19200  pgpfac1  19201  pgpfaclem3  19204  pgpfac  19205  ablfaclem2  19207  ablfaclem3  19208  ablfac  19209  cnmsubglem  20607  zlmlmod  20669  frgpcyg  20719  efsubm  25134  dchrghm  25831  dchr1  25832  dchrinv  25836  dchr1re  25838  dchrpt  25842  dchrsum2  25843  sumdchr2  25845  dchrhash  25846  dchr2sum  25848  rpvmasumlem  26062  rpvmasum2  26087  dchrisum0re  26088  fedgmullem2  31026  dvalveclem  38160  isnumbasgrplem1  39699  isnumbasabl  39704  isnumbasgrp  39705  dfacbasgrp  39706  isringrng  44151  rnglz  44154  isrnghm  44162  isrnghmd  44172  idrnghm  44178  c0rnghm  44183  zrrnghm  44187