Theorem idomringd 20688

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

Syntax hints:   → wi 4   ∈ wcel 2108  Ringcrg 20193  IDomncidom 20653

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-iota 6484  df-fv 6539  df-cring 20196  df-idom 20656

This theorem is referenced by:  fracfld  33302  dvdsruasso  33400  dvdsruasso2  33401  unitpidl1  33439  mxidlirredi  33486  mxidlirred  33487  rsprprmprmidlb  33538  rprmasso  33540  rprmasso2  33541  unitmulrprm  33543  rprmirred  33546  rprmirredb  33547  1arithidomlem1  33550  1arithidomlem2  33551  1arithidom  33552  pidufd  33558  1arithufdlem2  33560  1arithufdlem4  33562  dfufd2lem  33564  dfufd2  33565  r1pid2OLD  33618  assafld  33677  fldextrspunlem1  33716  algextdeglem7  33757  idomnnzpownz  42145  deg1gprod  42153  deg1pow  42154  aks6d1c6lem3  42185  unitscyglem5  42212