Theorem idomcringd 20612

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

Syntax hints:   → wi 4   ∈ wcel 2109   ∩ cin 3902  CRingccrg 20119  Domncdomn 20577  IDomncidom 20578

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 3438  df-in 3910  df-idom 20581

This theorem is referenced by:  idomringd  20613  subridom  33225  fracfld  33247  idomsubr  33248  dvdsruasso2  33323  rsprprmprmidlb  33460  rprmasso  33462  rprmasso2  33463  rprmirredlem  33467  rprmirred  33468  rprmirredb  33469  1arithidomlem1  33472  1arithidom  33474  1arithufdlem1  33481  1arithufdlem3  33483  1arithufdlem4  33484  dfufd2lem  33486  zringfrac  33491  ply1dg3rt0irred  33518  assafld  33604  fldextrspunfld  33643  unitscyglem5  42172  aks5lem7  42173