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

Theorem ablgrp 18398
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 18397 . 2 (𝐺 ∈ Abel ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ CMnd))
21simplbi 478 1 (𝐺 ∈ Abel → 𝐺 ∈ Grp)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2139  Grpcgrp 17623  CMndccmn 18393  Abelcabl 18394
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-v 3342  df-in 3722  df-abl 18396
This theorem is referenced by:  ablinvadd  18415  ablsub2inv  18416  ablsubadd  18417  ablsub4  18418  abladdsub4  18419  abladdsub  18420  ablpncan2  18421  ablpncan3  18422  ablsubsub  18423  ablsubsub4  18424  ablpnpcan  18425  ablnncan  18426  ablnnncan  18428  ablnnncan1  18429  ablsubsub23  18430  mulgdi  18432  mulgghm  18434  mulgsubdi  18435  ghmabl  18438  invghm  18439  eqgabl  18440  odadd1  18451  odadd2  18452  odadd  18453  gexexlem  18455  gexex  18456  torsubg  18457  oddvdssubg  18458  prdsabld  18465  cnaddinv  18474  cyggexb  18500  gsumsub  18548  telgsumfzslem  18585  telgsumfzs  18586  telgsums  18590  ablfacrp  18665  ablfac1lem  18667  ablfac1b  18669  ablfac1c  18670  ablfac1eulem  18671  ablfac1eu  18672  pgpfac1lem1  18673  pgpfac1lem2  18674  pgpfac1lem3a  18675  pgpfac1lem3  18676  pgpfac1lem4  18677  pgpfac1lem5  18678  pgpfac1  18679  pgpfaclem3  18682  pgpfac  18683  ablfaclem2  18685  ablfaclem3  18686  ablfac  18687  cnmsubglem  20011  zlmlmod  20073  frgpcyg  20124  efsubm  24496  dchrghm  25180  dchr1  25181  dchrinv  25185  dchr1re  25187  dchrpt  25191  dchrsum2  25192  sumdchr2  25194  dchrhash  25195  dchr2sum  25197  rpvmasumlem  25375  rpvmasum2  25400  dchrisum0re  25401  dvalveclem  36816  isnumbasgrplem1  38173  isnumbasabl  38178  isnumbasgrp  38179  dfacbasgrp  38180  isringrng  42391  rnglz  42394  isrnghm  42402  isrnghmd  42412  idrnghm  42418  c0rnghm  42423  zrrnghm  42427
  Copyright terms: Public domain W3C validator