Theorem isabl 19753

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2114  Grpcgrp 18903  CMndccmn 19749  Abelcabl 19750

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-in 3897  df-abl 19752

This theorem is referenced by:  ablgrp  19754  ablcmn  19756  isabl2  19759  ablpropd  19761  isabld  19764  ghmabl  19801  cntrabl  19812  prdsabld  19831  unitabl  20358  tsmsinv  24126  tgptsmscls  24128  tsmsxplem1  24131  tsmsxplem2  24132  abliso  33114  primrootsunit1  42553  gicabl  43548  2zrngaabl  48741  pgrpgt2nabl  48857