Theorem idomcringd 20658

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

Syntax hints:   → wi 4   ∈ wcel 2113   ∩ cin 3898  CRingccrg 20167  Domncdomn 20623  IDomncidom 20624

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 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-v 3440  df-in 3906  df-idom 20627

This theorem is referenced by:  idomringd  20659  domnprodeq0  33307  subridom  33317  fracfld  33339  idomsubr  33340  dvdsruasso2  33416  rsprprmprmidlb  33553  rprmasso  33555  rprmasso2  33556  rprmirredlem  33560  rprmirred  33561  rprmirredb  33562  1arithidomlem1  33565  1arithidom  33567  1arithufdlem1  33574  1arithufdlem3  33576  1arithufdlem4  33577  dfufd2lem  33579  zringfrac  33584  deg1prod  33613  ply1dg3rt0irred  33614  vietadeg1  33683  vietalem  33684  vieta  33685  assafld  33743  fldextrspunfld  33782  unitscyglem5  42392  aks5lem7  42393