Theorem isabl 19991

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   ∈ wcel 2145  Grpcgrp 19137  CMndccmn 19987  Abelcabl 19988

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-in 3906  df-abl 19990

This theorem is used by:  ablgrp  19992  ablcmn  19994  isabl2  19997  ablpropd  19999  isabld  20002  ghmabl  20039  cntrabl  20050  prdsabld  20069  unitabl  20607  tsmsinv  24460  tgptsmscls  24462  tsmsxplem1  24465  tsmsxplem2  24466  abliso  33589  primrootsunit1  43127  gicabl  44085  2zrngaabl  49316  pgrpgt2nabl  49447