Theorem idomcringd 20637

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

Syntax hints:   → wi 4   ∈ wcel 2111   ∩ cin 3896  CRingccrg 20147  Domncdomn 20602  IDomncidom 20603

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 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-in 3904  df-idom 20606

This theorem is referenced by:  idomringd  20638  subridom  33244  fracfld  33266  idomsubr  33267  dvdsruasso2  33343  rsprprmprmidlb  33480  rprmasso  33482  rprmasso2  33483  rprmirredlem  33487  rprmirred  33488  rprmirredb  33489  1arithidomlem1  33492  1arithidom  33494  1arithufdlem1  33501  1arithufdlem3  33503  1arithufdlem4  33504  dfufd2lem  33506  zringfrac  33511  ply1dg3rt0irred  33538  assafld  33642  fldextrspunfld  33681  unitscyglem5  42232  aks5lem7  42233