Theorem isabl 18910

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

Syntax hints:   ↔ wb 208   ∧ wa 398   ∈ wcel 2114  Grpcgrp 18103  CMndccmn 18906  Abelcabl 18907

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-in 3943  df-abl 18909

This theorem is referenced by:  ablgrp  18911  ablcmn  18913  isabl2  18915  ablpropd  18917  isabld  18920  ghmabl  18953  cntrabl  18963  prdsabld  18982  unitabl  19418  tsmsinv  22756  tgptsmscls  22758  tsmsxplem1  22761  tsmsxplem2  22762  abliso  30683  gicabl  39719  2zrngaabl  44235  pgrpgt2nabl  44434