Theorem ablgrp 13894

Description: An Abelian group is a group. (Contributed by NM, 26-Aug-2011.)

Assertion

Ref	Expression
ablgrp	|- ( G e. Abel -> G e. Grp )

Proof of Theorem ablgrp

Step	Hyp	Ref	Expression
1		isabl 13893	. 2 |- ( G e. Abel <-> ( G e. Grp /\ G e. CMnd ) )
2	1	simplbi 274	1 |- ( G e. Abel -> G e. Grp )

Syntax hints:   -> wi 4   e. wcel 2202   Grpcgrp 13601  CMndccmn 13889   Abelcabl 13890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-v 2804  df-in 3206  df-abl 13892

This theorem is referenced by:  ablgrpd  13895  ablinvadd  13915  ablsub2inv  13916  ablsubadd  13917  ablsub4  13918  abladdsub4  13919  abladdsub  13920  ablpncan2  13921  ablpncan3  13922  ablsubsub  13923  ablsubsub4  13924  ablpnpcan  13925  ablnncan  13926  ablnnncan  13928  ablnnncan1  13929  ablsubsub23  13930  ghmabl  13933  invghm  13934  eqgabl  13935  ablressid  13940  rnglz  13977  rngpropd  13987