Theorem isabl 19826

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2108  Grpcgrp 18973  CMndccmn 19822  Abelcabl 19823

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-in 3983  df-abl 19825

This theorem is referenced by:  ablgrp  19827  ablcmn  19829  isabl2  19832  ablpropd  19834  isabld  19837  ghmabl  19874  cntrabl  19885  prdsabld  19904  unitabl  20410  tsmsinv  24177  tgptsmscls  24179  tsmsxplem1  24182  tsmsxplem2  24183  abliso  33022  primrootsunit1  42054  gicabl  43056  2zrngaabl  47973  pgrpgt2nabl  48091