Theorem isabl 19770

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 19769	. 2 ⊢ Abel = (Grp ∩ CMnd)
2	1	elin2 4183	1 ⊢ (𝐺 ∈ Abel ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ CMnd))

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2109  Grpcgrp 18921  CMndccmn 19766  Abelcabl 19767

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-v 3466  df-in 3938  df-abl 19769

This theorem is referenced by:  ablgrp  19771  ablcmn  19773  isabl2  19776  ablpropd  19778  isabld  19781  ghmabl  19818  cntrabl  19829  prdsabld  19848  unitabl  20349  tsmsinv  24091  tgptsmscls  24093  tsmsxplem1  24096  tsmsxplem2  24097  abliso  33036  primrootsunit1  42115  gicabl  43090  2zrngaabl  48192  pgrpgt2nabl  48308