Theorem idomcringd 20699

Description: An integral domain is a commutative ring with unity. (Contributed by Thierry Arnoux, 4-May-2025.) Formerly subproof of idomringd 20700. (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 20668	. . 3 ⊢ IDomn = (CRing ∩ Domn)
3	1, 2	eleqtrdi 2849	. 2 ⊢ (𝜑 → 𝑅 ∈ (CRing ∩ Domn))
4	3	elin1d 4133	1 ⊢ (𝜑 → 𝑅 ∈ CRing)

Syntax hints:   → wi 4   ∈ wcel 2119   ∩ cin 3882  CRingccrg 20206  Domncdomn 20664  IDomncidom 20665

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433  df-in 3890  df-idom 20668

This theorem is referenced by:  idomringd  20700  domnprodeq0  33357  subridom  33367  fracfld  33392  idomsubr  33393  dvdsruasso2  33469  rsprprmprmidlb  33606  rprmasso  33608  rprmasso2  33609  rprmirredlem  33613  rprmirred  33614  rprmirredb  33615  1arithidomlem1  33618  1arithidom  33620  1arithufdlem1  33627  1arithufdlem3  33629  1arithufdlem4  33630  dfufd2lem  33632  zringfrac  33637  deg1prod  33666  ply1dg3rt0irred  33667  mplidomlem  33711  vietadeg1  33762  vietalem  33763  vieta  33764  assafld  33821  fldextrspunfld  33860  unitscyglem5  42684  aks5lem7  42685