Theorem isabl 19824

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

Syntax hints:   ↔ wb 208   ∧ wa 399   ∈ wcel 2142  Grpcgrp 18975  CMndccmn 19820  Abelcabl 19821

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-in 3911  df-abl 19823

This theorem is referenced by:  ablgrp  19825  ablcmn  19827  isabl2  19830  ablpropd  19832  isabld  19835  ghmabl  19872  cntrabl  19883  prdsabld  19902  unitabl  20429  tsmsinv  24205  tgptsmscls  24207  tsmsxplem1  24210  tsmsxplem2  24211  abliso  33211  primrootsunit1  42711  gicabl  43673  2zrngaabl  48869  pgrpgt2nabl  48985