Theorem isabl 18977

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

Syntax hints:   ↔ wb 209   ∧ wa 399   ∈ wcel 2111  Grpcgrp 18169  CMndccmn 18973  Abelcabl 18974

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-v 3411  df-in 3865  df-abl 18976

This theorem is referenced by:  ablgrp  18978  ablcmn  18980  isabl2  18982  ablpropd  18984  isabld  18987  ghmabl  19021  cntrabl  19031  prdsabld  19050  unitabl  19489  tsmsinv  22848  tgptsmscls  22850  tsmsxplem1  22853  tsmsxplem2  22854  abliso  30831  gicabl  40416  2zrngaabl  44935  pgrpgt2nabl  45135