Theorem isidom 20976

Description: An integral domain is a commutative domain. (Contributed by Mario Carneiro, 17-Jun-2015.)

Assertion

Ref	Expression
isidom	⊢ (𝑅 ∈ IDomn ↔ (𝑅 ∈ CRing ∧ 𝑅 ∈ Domn))

Proof of Theorem isidom

Step	Hyp	Ref	Expression
1		df-idom 20948	. 2 ⊢ IDomn = (CRing ∩ Domn)
2	1	elin2 4149	1 ⊢ (𝑅 ∈ IDomn ↔ (𝑅 ∈ CRing ∧ 𝑅 ∈ Domn))

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   ∈ wcel 2145  CRingccrg 20460  Domncdomn 20944  IDomncidom 20945

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 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-in 3906  df-idom 20948

This theorem is used by:  fldidom  21029  fiidomfld  21032  qsidomlem1  21636  qsidomlem2  21637  znfld  21866  znidomb  21867  ply1idom  26443  fta1glem1  26486  fta1glem2  26487  fta1g  26488  fta1b  26490  idomrootle  26491  lgsqrlem1  27673  lgsqrlem2  27674  lgsqrlem3  27675  lgsqrlem4  27676  idompropd  33842  subridom  33847  dvdsruasso  33940  zringidom  34083  mplidomlem  34159  idomnnzpownz  43182  idomnnzgmulnz  43183  aks6d1c5lem3  43187  aks6d1c5lem2  43188  deg1gprod  43190  deg1pow  43191  idomodle  44192  proot1mul  44195  proot1hash  44196  crngprmringdom  49438  idomcanl  49443  idomcanr  49444