Theorem isabl 19898

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   ∈ wcel 2146  Grpcgrp 19044  CMndccmn 19894  Abelcabl 19895

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 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-in 3913  df-abl 19897

This theorem is used by:  ablgrp  19899  ablcmn  19901  isabl2  19904  ablpropd  19906  isabld  19909  ghmabl  19946  cntrabl  19957  prdsabld  19976  unitabl  20512  tsmsinv  24356  tgptsmscls  24358  tsmsxplem1  24361  tsmsxplem2  24362  abliso  33419  primrootsunit1  42922  gicabl  43884  2zrngaabl  49072  pgrpgt2nabl  49203