Theorem isabl 18912

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

Syntax hints:   ↔ wb 208   ∧ wa 398   ∈ wcel 2114  Grpcgrp 18105  CMndccmn 18908  Abelcabl 18909

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 2795

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 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-v 3498  df-in 3945  df-abl 18911

This theorem is referenced by:  ablgrp  18913  ablcmn  18915  isabl2  18917  ablpropd  18919  isabld  18922  ghmabl  18955  cntrabl  18965  prdsabld  18984  unitabl  19420  tsmsinv  22758  tgptsmscls  22760  tsmsxplem1  22763  tsmsxplem2  22764  abliso  30685  gicabl  39706  2zrngaabl  44222  pgrpgt2nabl  44421