Theorem idomcringd 20687

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

Syntax hints:   → wi 4   ∈ wcel 2108   ∩ cin 3925  CRingccrg 20194  Domncdomn 20652  IDomncidom 20653

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-in 3933  df-idom 20656

This theorem is referenced by:  idomringd  20688  subridom  33280  fracfld  33302  idomsubr  33303  dvdsruasso2  33401  rsprprmprmidlb  33538  rprmasso  33540  rprmasso2  33541  rprmirredlem  33545  rprmirred  33546  rprmirredb  33547  1arithidomlem1  33550  1arithidom  33552  1arithufdlem1  33559  1arithufdlem3  33561  1arithufdlem4  33562  dfufd2lem  33564  zringfrac  33569  ply1dg3rt0irred  33595  assafld  33677  fldextrspunfld  33717  unitscyglem5  42212  aks5lem7  42213