Theorem ablgrp 13869

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

Syntax hints:   → wi 4   ∈ wcel 2200  Grpcgrp 13576  CMndccmn 13864  Abelcabl 13865

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2802  df-in 3204  df-abl 13867

This theorem is referenced by:  ablgrpd  13870  ablinvadd  13890  ablsub2inv  13891  ablsubadd  13892  ablsub4  13893  abladdsub4  13894  abladdsub  13895  ablpncan2  13896  ablpncan3  13897  ablsubsub  13898  ablsubsub4  13899  ablpnpcan  13900  ablnncan  13901  ablnnncan  13903  ablnnncan1  13904  ablsubsub23  13905  ghmabl  13908  invghm  13909  eqgabl  13910  ablressid  13915  rnglz  13951  rngpropd  13961