MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ablgrp Structured version   Visualization version   GIF version

Theorem ablgrp 18902
Description: An Abelian group is a group. (Contributed by NM, 26-Aug-2011.)
Assertion
Ref Expression
ablgrp (𝐺 ∈ Abel → 𝐺 ∈ Grp)

Proof of Theorem ablgrp
StepHypRef Expression
1 isabl 18901 . 2 (𝐺 ∈ Abel ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ CMnd))
21simplbi 501 1 (𝐺 ∈ Abel → 𝐺 ∈ Grp)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2114  Grpcgrp 18094  CMndccmn 18897  Abelcabl 18898
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 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2794
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2801  df-cleq 2815  df-clel 2894  df-v 3471  df-in 3915  df-abl 18900
This theorem is referenced by:  ablgrpd  18903  ablinvadd  18921  ablsub2inv  18922  ablsubadd  18923  ablsub4  18924  abladdsub4  18925  abladdsub  18926  ablpncan2  18927  ablpncan3  18928  ablsubsub  18929  ablsubsub4  18930  ablpnpcan  18931  ablnncan  18932  ablnnncan  18934  ablnnncan1  18935  ablsubsub23  18936  mulgdi  18938  mulgghm  18940  mulgsubdi  18941  ghmabl  18944  invghm  18945  eqgabl  18946  odadd1  18959  odadd2  18960  odadd  18961  gexexlem  18963  gexex  18964  torsubg  18965  oddvdssubg  18966  prdsabld  18973  cnaddinv  18982  cyggexb  19010  gsumsub  19059  telgsumfzslem  19099  telgsumfzs  19100  telgsums  19104  ablfacrp  19179  ablfac1lem  19181  ablfac1b  19183  ablfac1c  19184  ablfac1eulem  19185  ablfac1eu  19186  pgpfac1lem1  19187  pgpfac1lem2  19188  pgpfac1lem3a  19189  pgpfac1lem3  19190  pgpfac1lem4  19191  pgpfac1lem5  19192  pgpfac1  19193  pgpfaclem3  19196  pgpfac  19197  ablfaclem2  19199  ablfaclem3  19200  ablfac  19201  cnmsubglem  20152  zlmlmod  20214  frgpcyg  20263  efsubm  25141  dchrghm  25838  dchr1  25839  dchrinv  25843  dchr1re  25845  dchrpt  25849  dchrsum2  25850  sumdchr2  25852  dchrhash  25853  dchr2sum  25855  rpvmasumlem  26069  rpvmasum2  26094  dchrisum0re  26095  fedgmullem2  31083  dvalveclem  38279  isnumbasgrplem1  39975  isnumbasabl  39980  isnumbasgrp  39981  dfacbasgrp  39982  isringrng  44444  rnglz  44447  isrnghm  44455  isrnghmd  44465  idrnghm  44471  c0rnghm  44476  zrrnghm  44480
  Copyright terms: Public domain W3C validator