Theorem isabl 19691

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-in 3904  df-abl 19690

This theorem is referenced by:  ablgrp  19692  ablcmn  19694  isabl2  19697  ablpropd  19699  isabld  19702  ghmabl  19739  cntrabl  19750  prdsabld  19769  unitabl  20297  tsmsinv  24058  tgptsmscls  24060  tsmsxplem1  24063  tsmsxplem2  24064  abliso  33009  primrootsunit1  42130  gicabl  43132  2zrngaabl  48281  pgrpgt2nabl  48397