Theorem idomcringd 20704

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

Syntax hints:   → wi 4   ∈ wcel 2114   ∩ cin 3888  CRingccrg 20215  Domncdomn 20669  IDomncidom 20670

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-in 3896  df-idom 20673

This theorem is referenced by:  idomringd  20705  domnprodeq0  33337  subridom  33347  fracfld  33369  idomsubr  33370  dvdsruasso2  33446  rsprprmprmidlb  33583  rprmasso  33585  rprmasso2  33586  rprmirredlem  33590  rprmirred  33591  rprmirredb  33592  1arithidomlem1  33595  1arithidom  33597  1arithufdlem1  33604  1arithufdlem3  33606  1arithufdlem4  33607  dfufd2lem  33609  zringfrac  33614  deg1prod  33643  ply1dg3rt0irred  33644  vietadeg1  33722  vietalem  33723  vieta  33724  assafld  33781  fldextrspunfld  33820  unitscyglem5  42638  aks5lem7  42639