Theorem idomringd 20826

Description: An integral domain is a ring. (Contributed by Thierry Arnoux, 22-Mar-2025.)

Hypothesis

Ref	Expression
idomringd.1	⊢ (𝜑 → 𝑅 ∈ IDomn)

Assertion

Ref	Expression
idomringd	⊢ (𝜑 → 𝑅 ∈ Ring)

Proof of Theorem idomringd

Step	Hyp	Ref	Expression
1		idomringd.1	. . 3 ⊢ (𝜑 → 𝑅 ∈ IDomn)
2	1	idomcringd 20825	. 2 ⊢ (𝜑 → 𝑅 ∈ CRing)
3	2	crngringd 20323	1 ⊢ (𝜑 → 𝑅 ∈ Ring)

Syntax hints:   → wi 4   ∈ wcel 2143  Ringcrg 20310  IDomncidom 20792

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-iota 6492  df-fv 6544  df-cring 20313  df-idom 20795

This theorem is referenced by:  fracfld  33629  dvdsruasso  33698  dvdsruasso2  33699  mxidlirredi  33754  mxidlirred  33755  rprmasso  33815  rprmasso2  33816  unitmulrprm  33818  rprmirred  33821  rprmirredb  33822  1arithidomlem1  33825  1arithidomlem2  33826  1arithidom  33827  pidufd  33833  1arithufdlem2  33835  1arithufdlem4  33837  dfufd2lem  33839  dfufd2  33840  deg1prod  33873  mplidomlem  33917  vietadeg1  33968  vietalem  33969  vieta  33970  assafld  34027  fldextrspunlem1  34065  algextdeglem7  34113  idomnnzpownz  42899  deg1gprod  42907  deg1pow  42908  aks6d1c6lem3  42939  unitscyglem5  42966