Theorem idomcringd 20660

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

Syntax hints:   → wi 4   ∈ wcel 2113   ∩ cin 3900  CRingccrg 20169  Domncdomn 20625  IDomncidom 20626

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-in 3908  df-idom 20629

This theorem is referenced by:  idomringd  20661  domnprodeq0  33358  subridom  33368  fracfld  33390  idomsubr  33391  dvdsruasso2  33467  rsprprmprmidlb  33604  rprmasso  33606  rprmasso2  33607  rprmirredlem  33611  rprmirred  33612  rprmirredb  33613  1arithidomlem1  33616  1arithidom  33618  1arithufdlem1  33625  1arithufdlem3  33627  1arithufdlem4  33628  dfufd2lem  33630  zringfrac  33635  deg1prod  33664  ply1dg3rt0irred  33665  vietadeg1  33734  vietalem  33735  vieta  33736  assafld  33794  fldextrspunfld  33833  unitscyglem5  42453  aks5lem7  42454