Theorem idomcringd 20894

Description: An integral domain is a commutative ring with unity. (Contributed by Thierry Arnoux, 4-May-2025.) Formerly subproof of idomringd 20895. (Proof shortened by SN, 14-May-2025.)

Hypothesis

Ref	Expression
idomringd.1	⊢ (𝜑 → 𝑅 ∈ IDomn)

Assertion

Ref	Expression
idomcringd	⊢ (𝜑 → 𝑅 ∈ CRing)

Proof of Theorem idomcringd

Step	Hyp	Ref	Expression
1		idomringd.1	. . 3 ⊢ (𝜑 → 𝑅 ∈ IDomn)
2		df-idom 20864	. . 3 ⊢ IDomn = (CRing ∩ Domn)
3	1, 2	eleqtrdi 2872	. 2 ⊢ (𝜑 → 𝑅 ∈ (CRing ∩ Domn))
4	3	elin1d 4153	1 ⊢ (𝜑 → 𝑅 ∈ CRing)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   ∩ cin 3901  CRingccrg 20379  Domncdomn 20860  IDomncidom 20861

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 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3455  df-in 3909  df-idom 20864

This theorem is used by:  idomringd  20895  domnprodeq0  33727  subridom  33734  fracfld  33757  idomsubr  33758  dvdsruasso2  33827  mxidlirredi  33882  mxidlirred  33883  rprmasso  33943  rprmasso2  33944  rprmirredlem  33948  rprmirred  33949  rprmirredb  33950  1arithidomlem1  33953  1arithidom  33955  pidufd  33961  1arithufdlem1  33962  1arithufdlem3  33964  1arithufdlem4  33965  dfufd2lem  33967  zringfrac  33972  deg1prod  34001  ply1dg3rt0irred  34002  mplidomlem  34045  vietadeg1  34096  vietalem  34097  vieta  34098  assafld  34155  fldextrspunfld  34194  unitscyglem5  43073  aks5lem7  43074