Theorem isabl 19651

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

Syntax hints:   ↔ wb 205   ∧ wa 396   ∈ wcel 2106  Grpcgrp 18818  CMndccmn 19647  Abelcabl 19648

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-in 3955  df-abl 19650

This theorem is referenced by:  ablgrp  19652  ablcmn  19654  isabl2  19657  ablpropd  19659  isabld  19662  ghmabl  19699  cntrabl  19710  prdsabld  19729  unitabl  20197  tsmsinv  23651  tgptsmscls  23653  tsmsxplem1  23656  tsmsxplem2  23657  abliso  32192  gicabl  41831  2zrngaabl  46832  pgrpgt2nabl  47032