Theorem isabl 19682

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2109  Grpcgrp 18831  CMndccmn 19678  Abelcabl 19679

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 3440  df-in 3912  df-abl 19681

This theorem is referenced by:  ablgrp  19683  ablcmn  19685  isabl2  19688  ablpropd  19690  isabld  19693  ghmabl  19730  cntrabl  19741  prdsabld  19760  unitabl  20288  tsmsinv  24052  tgptsmscls  24054  tsmsxplem1  24057  tsmsxplem2  24058  abliso  33009  primrootsunit1  42090  gicabl  43092  2zrngaabl  48254  pgrpgt2nabl  48370