Theorem ablgrp 18903

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

Syntax hints:   → wi 4   ∈ wcel 2111  Grpcgrp 18095  CMndccmn 18898  Abelcabl 18899

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-abl 18901

This theorem is referenced by:  ablgrpd  18904  ablinvadd  18923  ablsub2inv  18924  ablsubadd  18925  ablsub4  18926  abladdsub4  18927  abladdsub  18928  ablpncan2  18929  ablpncan3  18930  ablsubsub  18931  ablsubsub4  18932  ablpnpcan  18933  ablnncan  18934  ablnnncan  18936  ablnnncan1  18937  ablsubsub23  18938  mulgdi  18940  mulgghm  18942  mulgsubdi  18943  ghmabl  18946  invghm  18947  eqgabl  18948  odadd1  18961  odadd2  18962  odadd  18963  gexexlem  18965  gexex  18966  torsubg  18967  oddvdssubg  18968  prdsabld  18975  cnaddinv  18984  cyggexb  19012  gsumsub  19061  telgsumfzslem  19101  telgsumfzs  19102  telgsums  19106  ablfacrp  19181  ablfac1lem  19183  ablfac1b  19185  ablfac1c  19186  ablfac1eulem  19187  ablfac1eu  19188  pgpfac1lem1  19189  pgpfac1lem2  19190  pgpfac1lem3a  19191  pgpfac1lem3  19192  pgpfac1lem4  19193  pgpfac1lem5  19194  pgpfac1  19195  pgpfaclem3  19198  pgpfac  19199  ablfaclem2  19201  ablfaclem3  19202  ablfac  19203  cnmsubglem  20154  zlmlmod  20216  frgpcyg  20265  efsubm  25143  dchrghm  25840  dchr1  25841  dchrinv  25845  dchr1re  25847  dchrpt  25851  dchrsum2  25852  sumdchr2  25854  dchrhash  25855  dchr2sum  25857  rpvmasumlem  26071  rpvmasum2  26096  dchrisum0re  26097  fedgmullem2  31114  dvalveclem  38321  isnumbasgrplem1  40045  isnumbasabl  40050  isnumbasgrp  40051  dfacbasgrp  40052  isringrng  44505  rnglz  44508  isrnghm  44516  isrnghmd  44526  idrnghm  44532  c0rnghm  44537  zrrnghm  44541