Theorem ablgrp 19999

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  Grpcgrp 19144  CMndccmn 19994  Abelcabl 19995

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-in 4091  df-abl 19997

This theorem is used by:  ablgrpd  20000  ablinvadd  20021  ablsub2inv  20022  ablsubadd  20023  ablsub4  20024  abladdsub4  20025  abladdsub  20026  ablsubadd23  20027  ablsubaddsub  20028  ablpncan2  20029  ablpncan3  20030  ablsubsub  20031  ablsubsub4  20032  ablpnpcan  20033  ablnncan  20034  ablnnncan  20036  ablnnncan1  20037  ablsubsub23  20038  mulgdi  20040  mulgghm  20042  mulgsubdi  20043  ghmabl  20046  invghm  20047  eqgabl  20048  odadd1  20062  odadd2  20063  odadd  20064  gexexlem  20066  gexex  20067  torsubg  20068  oddvdssubg  20069  prdsabld  20076  cnaddinv  20085  cyggexb  20113  gsumsub  20162  telgsumfzslem  20202  telgsumfzs  20203  telgsums  20207  ablfacrp  20282  ablfac1lem  20284  ablfac1b  20286  ablfac1c  20287  ablfac1eulem  20288  ablfac1eu  20289  pgpfac1lem1  20290  pgpfac1lem2  20291  pgpfac1lem3a  20292  pgpfac1lem3  20293  pgpfac1lem4  20294  pgpfac1lem5  20295  pgpfac1  20296  pgpfaclem3  20299  pgpfac  20300  ablfaclem2  20302  ablfaclem3  20303  ablfac  20304  rnglz  20387  rngpropd  20396  isringrng  20516  dfring2  20517  isrnghm  20671  isrnghmd  20681  idrnghm  20688  c0rnghm  20787  zrrnghm  20788  cnmsubglem  21736  zlmlmod  21828  frgpcyg  21879  efsubm  26879  dchrghm  27583  dchr1  27584  dchrinv  27588  dchr1re  27590  dchrpt  27594  dchrsum2  27595  sumdchr2  27597  dchrhash  27598  dchr2sum  27600  rpvmasumlem  27814  rpvmasum2  27839  dchrisum0re  27840  fedgmullem2  34262  dvalveclem  42083  primrootscoprbij  43153  primrootspoweq0  43157  isnumbasgrplem1  44103  isnumbasabl  44108  isnumbasgrp  44109  dfacbasgrp  44110