Theorem idomringd 20637

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

Syntax hints:   → wi 4   ∈ wcel 2109  Ringcrg 20142  IDomncidom 20602

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

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 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-iota 6464  df-fv 6519  df-cring 20145  df-idom 20605

This theorem is referenced by:  fracfld  33258  dvdsruasso  33356  dvdsruasso2  33357  unitpidl1  33395  mxidlirredi  33442  mxidlirred  33443  rsprprmprmidlb  33494  rprmasso  33496  rprmasso2  33497  unitmulrprm  33499  rprmirred  33502  rprmirredb  33503  1arithidomlem1  33506  1arithidomlem2  33507  1arithidom  33508  pidufd  33514  1arithufdlem2  33516  1arithufdlem4  33518  dfufd2lem  33520  dfufd2  33521  r1pid2OLD  33574  assafld  33633  fldextrspunlem1  33670  algextdeglem7  33713  idomnnzpownz  42120  deg1gprod  42128  deg1pow  42129  aks6d1c6lem3  42160  unitscyglem5  42187