Theorem idomcringd 20695

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

Syntax hints:   → wi 4   ∈ wcel 2114   ∩ cin 3889  CRingccrg 20206  Domncdomn 20660  IDomncidom 20661

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-in 3897  df-idom 20664

This theorem is referenced by:  idomringd  20696  domnprodeq0  33352  subridom  33362  fracfld  33384  idomsubr  33385  dvdsruasso2  33461  rsprprmprmidlb  33598  rprmasso  33600  rprmasso2  33601  rprmirredlem  33605  rprmirred  33606  rprmirredb  33607  1arithidomlem1  33610  1arithidom  33612  1arithufdlem1  33619  1arithufdlem3  33621  1arithufdlem4  33622  dfufd2lem  33624  zringfrac  33629  deg1prod  33658  ply1dg3rt0irred  33659  vietadeg1  33737  vietalem  33738  vieta  33739  assafld  33797  fldextrspunfld  33836  unitscyglem5  42652  aks5lem7  42653