Theorem isabl 20049

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   ∈ wcel 2147  Grpcgrp 19194  CMndccmn 20045  Abelcabl 20046

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-in 4094  df-abl 20048

This theorem is used by:  ablgrp  20050  ablcmn  20052  isabl2  20055  ablpropd  20057  isabld  20060  ghmabl  20097  cntrabl  20108  prdsabld  20127  unitabl  20665  tsmsinv  24522  tgptsmscls  24524  tsmsxplem1  24527  tsmsxplem2  24528  abliso  33695  primrootsunit1  43413  gicabl  44367  2zrngaabl  49620  pgrpgt2nabl  49809