Theorem ablgrp 19581

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

Syntax hints:   → wi 4   ∈ wcel 2106  Grpcgrp 18762  CMndccmn 19576  Abelcabl 19577

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3448  df-in 3920  df-abl 19579

This theorem is referenced by:  ablgrpd  19582  ablinvadd  19602  ablsub2inv  19603  ablsubadd  19604  ablsub4  19605  abladdsub4  19606  abladdsub  19607  ablpncan2  19608  ablpncan3  19609  ablsubsub  19610  ablsubsub4  19611  ablpnpcan  19612  ablnncan  19613  ablnnncan  19615  ablnnncan1  19616  ablsubsub23  19617  mulgdi  19619  mulgghm  19621  mulgsubdi  19622  ghmabl  19625  invghm  19626  eqgabl  19627  odadd1  19640  odadd2  19641  odadd  19642  gexexlem  19644  gexex  19645  torsubg  19646  oddvdssubg  19647  prdsabld  19654  cnaddinv  19663  cyggexb  19690  gsumsub  19739  telgsumfzslem  19779  telgsumfzs  19780  telgsums  19784  ablfacrp  19859  ablfac1lem  19861  ablfac1b  19863  ablfac1c  19864  ablfac1eulem  19865  ablfac1eu  19866  pgpfac1lem1  19867  pgpfac1lem2  19868  pgpfac1lem3a  19869  pgpfac1lem3  19870  pgpfac1lem4  19871  pgpfac1lem5  19872  pgpfac1  19873  pgpfaclem3  19876  pgpfac  19877  ablfaclem2  19879  ablfaclem3  19880  ablfac  19881  cnmsubglem  20897  zlmlmod  20964  frgpcyg  21017  efsubm  25944  dchrghm  26641  dchr1  26642  dchrinv  26646  dchr1re  26648  dchrpt  26652  dchrsum2  26653  sumdchr2  26655  dchrhash  26656  dchr2sum  26658  rpvmasumlem  26872  rpvmasum2  26897  dchrisum0re  26898  fedgmullem2  32412  dvalveclem  39561  isnumbasgrplem1  41486  isnumbasabl  41491  isnumbasgrp  41492  dfacbasgrp  41493  isringrng  46299  rnglz  46302  isrnghm  46310  isrnghmd  46320  idrnghm  46326  c0rnghm  46331  zrrnghm  46335