Theorem isabl 19911

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   ∈ wcel 2145  Grpcgrp 19057  CMndccmn 19907  Abelcabl 19908

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-in 3906  df-abl 19910

This theorem is used by:  ablgrp  19912  ablcmn  19914  isabl2  19917  ablpropd  19919  isabld  19922  ghmabl  19959  cntrabl  19970  prdsabld  19989  unitabl  20525  tsmsinv  24374  tgptsmscls  24376  tsmsxplem1  24379  tsmsxplem2  24380  abliso  33475  primrootsunit1  42963  gicabl  43940  2zrngaabl  49165  pgrpgt2nabl  49296