Theorem ablgrp 13899

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

Syntax hints:   → wi 4   ∈ wcel 2201  Grpcgrp 13606  CMndccmn 13894  Abelcabl 13895

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 2212

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1810  df-clab 2217  df-cleq 2223  df-clel 2226  df-nfc 2362  df-v 2803  df-in 3205  df-abl 13897

This theorem is referenced by:  ablgrpd  13900  ablinvadd  13920  ablsub2inv  13921  ablsubadd  13922  ablsub4  13923  abladdsub4  13924  abladdsub  13925  ablpncan2  13926  ablpncan3  13927  ablsubsub  13928  ablsubsub4  13929  ablpnpcan  13930  ablnncan  13931  ablnnncan  13933  ablnnncan1  13934  ablsubsub23  13935  ghmabl  13938  invghm  13939  eqgabl  13940  ablressid  13945  rnglz  13982  rngpropd  13992