Theorem idomringd 20745

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

Syntax hints:   → wi 4   ∈ wcel 2106  Ringcrg 20251  IDomncidom 20710

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-iota 6516  df-fv 6571  df-cring 20254  df-idom 20713

This theorem is referenced by:  fracfld  33290  dvdsruasso  33393  dvdsruasso2  33394  unitpidl1  33432  mxidlirredi  33479  mxidlirred  33480  rsprprmprmidlb  33531  rprmasso  33533  rprmasso2  33534  unitmulrprm  33536  rprmirred  33539  rprmirredb  33540  1arithidomlem1  33543  1arithidomlem2  33544  1arithidom  33545  pidufd  33551  1arithufdlem2  33553  1arithufdlem4  33555  dfufd2lem  33557  dfufd2  33558  r1pid2OLD  33609  assafld  33665  algextdeglem7  33729  idomnnzpownz  42114  deg1gprod  42122  deg1pow  42123  aks6d1c6lem3  42154  unitscyglem5  42181