Theorem ablgrp 18198

Description: An Abelian group is a group. (Contributed by NM, 26-Aug-2011.)

Assertion

Ref	Expression
ablgrp	|- ( G e. Abel -> G e. Grp )

Proof of Theorem ablgrp

Step	Hyp	Ref	Expression
1		isabl 18197	. 2 |- ( G e. Abel <-> ( G e. Grp /\ G e. CMnd ) )
2	1	simplbi 476	1 |- ( G e. Abel -> G e. Grp )

Syntax hints:   -> wi 4   e. wcel 1990   Grpcgrp 17422  CMndccmn 18193   Abelcabl 18194

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-in 3581  df-abl 18196

This theorem is referenced by:  ablinvadd  18215  ablsub2inv  18216  ablsubadd  18217  ablsub4  18218  abladdsub4  18219  abladdsub  18220  ablpncan2  18221  ablpncan3  18222  ablsubsub  18223  ablsubsub4  18224  ablpnpcan  18225  ablnncan  18226  ablnnncan  18228  ablnnncan1  18229  ablsubsub23  18230  mulgdi  18232  mulgghm  18234  mulgsubdi  18235  ghmabl  18238  invghm  18239  eqgabl  18240  odadd1  18251  odadd2  18252  odadd  18253  gexexlem  18255  gexex  18256  torsubg  18257  oddvdssubg  18258  prdsabld  18265  cnaddinv  18274  cyggexb  18300  gsumsub  18348  telgsumfzslem  18385  telgsumfzs  18386  telgsums  18390  ablfacrp  18465  ablfac1lem  18467  ablfac1b  18469  ablfac1c  18470  ablfac1eulem  18471  ablfac1eu  18472  pgpfac1lem1  18473  pgpfac1lem2  18474  pgpfac1lem3a  18475  pgpfac1lem3  18476  pgpfac1lem4  18477  pgpfac1lem5  18478  pgpfac1  18479  pgpfaclem3  18482  pgpfac  18483  ablfaclem2  18485  ablfaclem3  18486  ablfac  18487  cnmsubglem  19809  zlmlmod  19871  frgpcyg  19922  efsubm  24297  dchrghm  24981  dchr1  24982  dchrinv  24986  dchr1re  24988  dchrpt  24992  dchrsum2  24993  sumdchr2  24995  dchrhash  24996  dchr2sum  24998  rpvmasumlem  25176  rpvmasum2  25201  dchrisum0re  25202  dvalveclem  36314  isnumbasgrplem1  37671  isnumbasabl  37676  isnumbasgrp  37677  dfacbasgrp  37678  isringrng  41881  rnglz  41884  isrnghm  41892  isrnghmd  41902  idrnghm  41908  c0rnghm  41913  zrrnghm  41917