Theorem idomringd 20700

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 20699	. 2 ⊢ (𝜑 → 𝑅 ∈ CRing)
3	2	crngringd 20218	1 ⊢ (𝜑 → 𝑅 ∈ Ring)

Syntax hints:   → wi 4   ∈ wcel 2119  Ringcrg 20205  IDomncidom 20665

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-iota 6441  df-fv 6493  df-cring 20208  df-idom 20668

This theorem is referenced by:  fracfld  33392  dvdsruasso  33468  dvdsruasso2  33469  unitpidl1  33507  mxidlirredi  33554  mxidlirred  33555  rsprprmprmidlb  33606  rprmasso  33608  rprmasso2  33609  unitmulrprm  33611  rprmirred  33614  rprmirredb  33615  1arithidomlem1  33618  1arithidomlem2  33619  1arithidom  33620  pidufd  33626  1arithufdlem2  33628  1arithufdlem4  33630  dfufd2lem  33632  dfufd2  33633  deg1prod  33666  r1pid2OLD  33692  mplidomlem  33711  vietadeg1  33762  vietalem  33763  vieta  33764  assafld  33821  fldextrspunlem1  33859  algextdeglem7  33907  idomnnzpownz  42617  deg1gprod  42625  deg1pow  42626  aks6d1c6lem3  42657  unitscyglem5  42684