Theorem idomcringd 20636

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

Syntax hints:   → wi 4   ∈ wcel 2109   ∩ cin 3913  CRingccrg 20143  Domncdomn 20601  IDomncidom 20602

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-in 3921  df-idom 20605

This theorem is referenced by:  idomringd  20637  subridom  33236  fracfld  33258  idomsubr  33259  dvdsruasso2  33357  rsprprmprmidlb  33494  rprmasso  33496  rprmasso2  33497  rprmirredlem  33501  rprmirred  33502  rprmirredb  33503  1arithidomlem1  33506  1arithidom  33508  1arithufdlem1  33515  1arithufdlem3  33517  1arithufdlem4  33518  dfufd2lem  33520  zringfrac  33525  ply1dg3rt0irred  33551  assafld  33633  fldextrspunfld  33671  unitscyglem5  42187  aks5lem7  42188