Theorem idomcringd 20773

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

Syntax hints:   → wi 4   ∈ wcel 2142   ∩ cin 3903  CRingccrg 20280  Domncdomn 20738  IDomncidom 20739

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-in 3911  df-idom 20742

This theorem is referenced by:  idomringd  20774  domnprodeq0  33457  subridom  33467  fracfld  33492  idomsubr  33493  dvdsruasso2  33569  mxidlirredi  33656  mxidlirred  33657  rprmasso  33718  rprmasso2  33719  rprmirredlem  33723  rprmirred  33724  rprmirredb  33725  1arithidomlem1  33728  1arithidom  33730  pidufd  33736  1arithufdlem1  33737  1arithufdlem3  33739  1arithufdlem4  33740  dfufd2lem  33742  zringfrac  33747  deg1prod  33776  ply1dg3rt0irred  33777  mplidomlem  33821  vietadeg1  33872  vietalem  33873  vieta  33874  assafld  33931  fldextrspunfld  33970  unitscyglem5  42813  aks5lem7  42814