Theorem isidom 20875

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 20847	. 2 ⊢ IDomn = (CRing ∩ Domn)
2	1	elin2 4156	1 ⊢ (𝑅 ∈ IDomn ↔ (𝑅 ∈ CRing ∧ 𝑅 ∈ Domn))

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   ∈ wcel 2146  CRingccrg 20362  Domncdomn 20843  IDomncidom 20844

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 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-in 3913  df-idom 20847

This theorem is used by:  fldidom  20927  fiidomfld  20930  qsidomlem1  21532  qsidomlem2  21533  znfld  21762  znidomb  21763  ply1idom  26335  fta1glem1  26378  fta1glem2  26379  fta1g  26380  fta1b  26382  idomrootle  26383  lgsqrlem1  27563  lgsqrlem2  27564  lgsqrlem3  27565  lgsqrlem4  27566  idompropd  33667  subridom  33672  dvdsruasso  33764  zringidom  33907  mplidomlem  33983  idomnnzpownz  42959  idomnnzgmulnz  42960  aks6d1c5lem3  42964  aks6d1c5lem2  42965  deg1gprod  42967  deg1pow  42968  idomodle  43978  proot1mul  43981  proot1hash  43982  crngprmringdom  49166  idomcanl  49171  idomcanr  49172