Theorem idomcringd 20744

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

Syntax hints:   → wi 4   ∈ wcel 2106   ∩ cin 3962  CRingccrg 20252  Domncdomn 20709  IDomncidom 20710

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-v 3480  df-in 3970  df-idom 20713

This theorem is referenced by:  idomringd  20745  subridom  33270  fracfld  33290  idomsubr  33291  dvdsruasso2  33394  rsprprmprmidlb  33531  rprmasso  33533  rprmasso2  33534  rprmirredlem  33538  rprmirred  33539  rprmirredb  33540  1arithidomlem1  33543  1arithidom  33545  1arithufdlem1  33552  1arithufdlem3  33554  1arithufdlem4  33555  dfufd2lem  33557  zringfrac  33562  ply1dg3rt0irred  33587  assafld  33665  unitscyglem5  42181  aks5lem7  42182