Theorem isabl 20007

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   ∈ wcel 2144  Grpcgrp 19153  CMndccmn 20003  Abelcabl 20004

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-in 4090  df-abl 20006

This theorem is used by:  ablgrp  20008  ablcmn  20010  isabl2  20013  ablpropd  20015  isabld  20018  ghmabl  20055  cntrabl  20066  prdsabld  20085  unitabl  20623  tsmsinv  24476  tgptsmscls  24478  tsmsxplem1  24481  tsmsxplem2  24482  abliso  33646  primrootsunit1  43256  gicabl  44210  2zrngaabl  49455  pgrpgt2nabl  49586