Theorem isabl 19690

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2109  Grpcgrp 18841  CMndccmn 19686  Abelcabl 19687

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 3446  df-in 3918  df-abl 19689

This theorem is referenced by:  ablgrp  19691  ablcmn  19693  isabl2  19696  ablpropd  19698  isabld  19701  ghmabl  19738  cntrabl  19749  prdsabld  19768  unitabl  20269  tsmsinv  24011  tgptsmscls  24013  tsmsxplem1  24016  tsmsxplem2  24017  abliso  32950  primrootsunit1  42058  gicabl  43061  2zrngaabl  48211  pgrpgt2nabl  48327