Theorem ablgrp 18405

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

Syntax hints:   → wi 4   ∈ wcel 2145  Grpcgrp 17630  CMndccmn 18400  Abelcabl 18401

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-v 3353  df-in 3730  df-abl 18403

This theorem is referenced by:  ablinvadd  18422  ablsub2inv  18423  ablsubadd  18424  ablsub4  18425  abladdsub4  18426  abladdsub  18427  ablpncan2  18428  ablpncan3  18429  ablsubsub  18430  ablsubsub4  18431  ablpnpcan  18432  ablnncan  18433  ablnnncan  18435  ablnnncan1  18436  ablsubsub23  18437  mulgdi  18439  mulgghm  18441  mulgsubdi  18442  ghmabl  18445  invghm  18446  eqgabl  18447  odadd1  18458  odadd2  18459  odadd  18460  gexexlem  18462  gexex  18463  torsubg  18464  oddvdssubg  18465  prdsabld  18472  cnaddinv  18481  cyggexb  18507  gsumsub  18555  telgsumfzslem  18593  telgsumfzs  18594  telgsums  18598  ablfacrp  18673  ablfac1lem  18675  ablfac1b  18677  ablfac1c  18678  ablfac1eulem  18679  ablfac1eu  18680  pgpfac1lem1  18681  pgpfac1lem2  18682  pgpfac1lem3a  18683  pgpfac1lem3  18684  pgpfac1lem4  18685  pgpfac1lem5  18686  pgpfac1  18687  pgpfaclem3  18690  pgpfac  18691  ablfaclem2  18693  ablfaclem3  18694  ablfac  18695  cnmsubglem  20024  zlmlmod  20086  frgpcyg  20137  efsubm  24518  dchrghm  25202  dchr1  25203  dchrinv  25207  dchr1re  25209  dchrpt  25213  dchrsum2  25214  sumdchr2  25216  dchrhash  25217  dchr2sum  25219  rpvmasumlem  25397  rpvmasum2  25422  dchrisum0re  25423  dvalveclem  36835  isnumbasgrplem1  38197  isnumbasabl  38202  isnumbasgrp  38203  dfacbasgrp  38204  isringrng  42409  rnglz  42412  isrnghm  42420  isrnghmd  42430  idrnghm  42436  c0rnghm  42441  zrrnghm  42445