Theorem isabl 19849

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

Syntax hints:   ↔ wb 209   ∧ wa 400   ∈ wcel 2143  Grpcgrp 18995  CMndccmn 19845  Abelcabl 19846

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-in 3912  df-abl 19848

This theorem is referenced by:  ablgrp  19850  ablcmn  19852  isabl2  19855  ablpropd  19857  isabld  19860  ghmabl  19897  cntrabl  19908  prdsabld  19927  unitabl  20462  tsmsinv  24305  tgptsmscls  24307  tsmsxplem1  24310  tsmsxplem2  24311  abliso  33355  primrootsunit1  42864  gicabl  43826  2zrngaabl  49015  pgrpgt2nabl  49146