Theorem ablgrp 14027

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

Syntax hints:   → wi 4   ∈ wcel 2205  Grpcgrp 13734  CMndccmn 14022  Abelcabl 14023

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-v 2817  df-in 3219  df-abl 14025

This theorem is referenced by:  ablgrpd  14028  ablinvadd  14048  ablsub2inv  14049  ablsubadd  14050  ablsub4  14051  abladdsub4  14052  abladdsub  14053  ablpncan2  14054  ablpncan3  14055  ablsubsub  14056  ablsubsub4  14057  ablpnpcan  14058  ablnncan  14059  ablnnncan  14061  ablnnncan1  14062  ablsubsub23  14063  ghmabl  14066  invghm  14067  eqgabl  14068  ablressid  14073  rnglz  14110  rngpropd  14120