Theorem isabl 19771

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-v 3465  df-in 3938  df-abl 19770

This theorem is referenced by:  ablgrp  19772  ablcmn  19774  isabl2  19777  ablpropd  19779  isabld  19782  ghmabl  19819  cntrabl  19830  prdsabld  19849  unitabl  20353  tsmsinv  24103  tgptsmscls  24105  tsmsxplem1  24108  tsmsxplem2  24109  abliso  32985  primrootsunit1  42073  gicabl  43089  2zrngaabl  48139  pgrpgt2nabl  48255