Theorem ablgrp 19916

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  Grpcgrp 19061  CMndccmn 19911  Abelcabl 19912

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3455  df-in 3909  df-abl 19914

This theorem is used by:  ablgrpd  19917  ablinvadd  19938  ablsub2inv  19939  ablsubadd  19940  ablsub4  19941  abladdsub4  19942  abladdsub  19943  ablsubadd23  19944  ablsubaddsub  19945  ablpncan2  19946  ablpncan3  19947  ablsubsub  19948  ablsubsub4  19949  ablpnpcan  19950  ablnncan  19951  ablnnncan  19953  ablnnncan1  19954  ablsubsub23  19955  mulgdi  19957  mulgghm  19959  mulgsubdi  19960  ghmabl  19963  invghm  19964  eqgabl  19965  odadd1  19979  odadd2  19980  odadd  19981  gexexlem  19983  gexex  19984  torsubg  19985  oddvdssubg  19986  prdsabld  19993  cnaddinv  20002  cyggexb  20030  gsumsub  20079  telgsumfzslem  20119  telgsumfzs  20120  telgsums  20124  ablfacrp  20199  ablfac1lem  20201  ablfac1b  20203  ablfac1c  20204  ablfac1eulem  20205  ablfac1eu  20206  pgpfac1lem1  20207  pgpfac1lem2  20208  pgpfac1lem3a  20209  pgpfac1lem3  20210  pgpfac1lem4  20211  pgpfac1lem5  20212  pgpfac1  20213  pgpfaclem3  20216  pgpfac  20217  ablfaclem2  20219  ablfaclem3  20220  ablfac  20221  rnglz  20304  rngpropd  20313  isringrng  20432  dfring2  20433  isrnghm  20586  isrnghmd  20596  idrnghm  20603  c0rnghm  20701  zrrnghm  20702  cnmsubglem  21647  zlmlmod  21739  frgpcyg  21790  efsubm  26789  dchrghm  27493  dchr1  27494  dchrinv  27498  dchr1re  27500  dchrpt  27504  dchrsum2  27505  sumdchr2  27507  dchrhash  27508  dchr2sum  27510  rpvmasumlem  27724  rpvmasum2  27749  dchrisum0re  27750  fedgmullem2  34142  dvalveclem  41900  primrootscoprbij  42970  primrootspoweq0  42974  isnumbasgrplem1  43944  isnumbasabl  43949  isnumbasgrp  43950  dfacbasgrp  43951