Theorem isabl 19853

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

Syntax hints:   ↔ wb 209   ∧ wa 400   ∈ wcel 2149  Grpcgrp 18999  CMndccmn 19849  Abelcabl 19850

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-in 3920  df-abl 19852

This theorem is referenced by:  ablgrp  19854  ablcmn  19856  isabl2  19859  ablpropd  19861  isabld  19864  ghmabl  19901  cntrabl  19912  prdsabld  19931  unitabl  20465  tsmsinv  24273  tgptsmscls  24275  tsmsxplem1  24278  tsmsxplem2  24279  abliso  33295  primrootsunit1  42753  gicabl  43717  2zrngaabl  48903  pgrpgt2nabl  49030