Theorem isabl 19714

Description: The predicate "is an Abelian (commutative) group". (Contributed by NM, 17-Oct-2011.)

Assertion

Ref	Expression
isabl	⊢ (𝐺 ∈ Abel ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ CMnd))

Proof of Theorem isabl

Step	Hyp	Ref	Expression
1		df-abl 19713	. 2 ⊢ Abel = (Grp ∩ CMnd)
2	1	elin2 4166	1 ⊢ (𝐺 ∈ Abel ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ CMnd))

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2109  Grpcgrp 18865  CMndccmn 19710  Abelcabl 19711

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-in 3921  df-abl 19713

This theorem is referenced by:  ablgrp  19715  ablcmn  19717  isabl2  19720  ablpropd  19722  isabld  19725  ghmabl  19762  cntrabl  19773  prdsabld  19792  unitabl  20293  tsmsinv  24035  tgptsmscls  24037  tsmsxplem1  24040  tsmsxplem2  24041  abliso  32977  primrootsunit1  42085  gicabl  43088  2zrngaabl  48238  pgrpgt2nabl  48354