Theorem ablgrp 18584

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

Syntax hints:   → wi 4   ∈ wcel 2107  Grpcgrp 17809  CMndccmn 18579  Abelcabl 18580

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-v 3400  df-in 3799  df-abl 18582

This theorem is referenced by:  ablinvadd  18601  ablsub2inv  18602  ablsubadd  18603  ablsub4  18604  abladdsub4  18605  abladdsub  18606  ablpncan2  18607  ablpncan3  18608  ablsubsub  18609  ablsubsub4  18610  ablpnpcan  18611  ablnncan  18612  ablnnncan  18614  ablnnncan1  18615  ablsubsub23  18616  mulgdi  18618  mulgghm  18620  mulgsubdi  18621  ghmabl  18624  invghm  18625  eqgabl  18626  odadd1  18637  odadd2  18638  odadd  18639  gexexlem  18641  gexex  18642  torsubg  18643  oddvdssubg  18644  prdsabld  18651  cnaddinv  18660  cyggexb  18686  gsumsub  18734  telgsumfzslem  18772  telgsumfzs  18773  telgsums  18777  ablfacrp  18852  ablfac1lem  18854  ablfac1b  18856  ablfac1c  18857  ablfac1eulem  18858  ablfac1eu  18859  pgpfac1lem1  18860  pgpfac1lem2  18861  pgpfac1lem3a  18862  pgpfac1lem3  18863  pgpfac1lem4  18864  pgpfac1lem5  18865  pgpfac1  18866  pgpfaclem3  18869  pgpfac  18870  ablfaclem2  18872  ablfaclem3  18873  ablfac  18874  cnmsubglem  20205  zlmlmod  20267  frgpcyg  20317  efsubm  24735  dchrghm  25433  dchr1  25434  dchrinv  25438  dchr1re  25440  dchrpt  25444  dchrsum2  25445  sumdchr2  25447  dchrhash  25448  dchr2sum  25450  rpvmasumlem  25628  rpvmasum2  25653  dchrisum0re  25654  dvalveclem  37179  isnumbasgrplem1  38630  isnumbasabl  38635  isnumbasgrp  38636  dfacbasgrp  38637  isringrng  42896  rnglz  42899  isrnghm  42907  isrnghmd  42917  idrnghm  42923  c0rnghm  42928  zrrnghm  42932