Theorem ablgrp 19817

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

Syntax hints:   → wi 4   ∈ wcel 2105  Grpcgrp 18963  CMndccmn 19812  Abelcabl 19813

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-in 3969  df-abl 19815

This theorem is referenced by:  ablgrpd  19818  ablinvadd  19839  ablsub2inv  19840  ablsubadd  19841  ablsub4  19842  abladdsub4  19843  abladdsub  19844  ablsubadd23  19845  ablsubaddsub  19846  ablpncan2  19847  ablpncan3  19848  ablsubsub  19849  ablsubsub4  19850  ablpnpcan  19851  ablnncan  19852  ablnnncan  19854  ablnnncan1  19855  ablsubsub23  19856  mulgdi  19858  mulgghm  19860  mulgsubdi  19861  ghmabl  19864  invghm  19865  eqgabl  19866  odadd1  19880  odadd2  19881  odadd  19882  gexexlem  19884  gexex  19885  torsubg  19886  oddvdssubg  19887  prdsabld  19894  cnaddinv  19903  cyggexb  19931  gsumsub  19980  telgsumfzslem  20020  telgsumfzs  20021  telgsums  20025  ablfacrp  20100  ablfac1lem  20102  ablfac1b  20104  ablfac1c  20105  ablfac1eulem  20106  ablfac1eu  20107  pgpfac1lem1  20108  pgpfac1lem2  20109  pgpfac1lem3a  20110  pgpfac1lem3  20111  pgpfac1lem4  20112  pgpfac1lem5  20113  pgpfac1  20114  pgpfaclem3  20117  pgpfac  20118  ablfaclem2  20120  ablfaclem3  20121  ablfac  20122  rnglz  20182  rngpropd  20191  isringrng  20300  isrnghm  20457  isrnghmd  20467  idrnghm  20474  c0rnghm  20551  zrrnghm  20552  cnmsubglem  21465  zlmlmod  21554  frgpcyg  21609  efsubm  26607  dchrghm  27314  dchr1  27315  dchrinv  27319  dchr1re  27321  dchrpt  27325  dchrsum2  27326  sumdchr2  27328  dchrhash  27329  dchr2sum  27331  rpvmasumlem  27545  rpvmasum2  27570  dchrisum0re  27571  fedgmullem2  33657  dvalveclem  41007  primrootscoprbij  42083  primrootspoweq0  42087  isnumbasgrplem1  43089  isnumbasabl  43094  isnumbasgrp  43095  dfacbasgrp  43096