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

Theorem ablgrp 18842
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 18841 . 2 (𝐺 ∈ Abel ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ CMnd))
21simplbi 498 1 (𝐺 ∈ Abel → 𝐺 ∈ Grp)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2105  Grpcgrp 18043  CMndccmn 18837  Abelcabl 18838
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3497  df-in 3942  df-abl 18840
This theorem is referenced by:  ablgrpd  18843  ablinvadd  18861  ablsub2inv  18862  ablsubadd  18863  ablsub4  18864  abladdsub4  18865  abladdsub  18866  ablpncan2  18867  ablpncan3  18868  ablsubsub  18869  ablsubsub4  18870  ablpnpcan  18871  ablnncan  18872  ablnnncan  18874  ablnnncan1  18875  ablsubsub23  18876  mulgdi  18878  mulgghm  18880  mulgsubdi  18881  ghmabl  18884  invghm  18885  eqgabl  18886  odadd1  18899  odadd2  18900  odadd  18901  gexexlem  18903  gexex  18904  torsubg  18905  oddvdssubg  18906  prdsabld  18913  cnaddinv  18922  cyggexb  18950  gsumsub  18999  telgsumfzslem  19039  telgsumfzs  19040  telgsums  19044  ablfacrp  19119  ablfac1lem  19121  ablfac1b  19123  ablfac1c  19124  ablfac1eulem  19125  ablfac1eu  19126  pgpfac1lem1  19127  pgpfac1lem2  19128  pgpfac1lem3a  19129  pgpfac1lem3  19130  pgpfac1lem4  19131  pgpfac1lem5  19132  pgpfac1  19133  pgpfaclem3  19136  pgpfac  19137  ablfaclem2  19139  ablfaclem3  19140  ablfac  19141  cnmsubglem  20538  zlmlmod  20600  frgpcyg  20650  efsubm  25062  dchrghm  25760  dchr1  25761  dchrinv  25765  dchr1re  25767  dchrpt  25771  dchrsum2  25772  sumdchr2  25774  dchrhash  25775  dchr2sum  25777  rpvmasumlem  25991  rpvmasum2  26016  dchrisum0re  26017  fedgmullem2  30926  dvalveclem  38043  isnumbasgrplem1  39581  isnumbasabl  39586  isnumbasgrp  39587  dfacbasgrp  39588  isringrng  44050  rnglz  44053  isrnghm  44061  isrnghmd  44071  idrnghm  44077  c0rnghm  44082  zrrnghm  44086
  Copyright terms: Public domain W3C validator