Theorem idomringd 20889

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  Ringcrg 20372  IDomncidom 20855

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6489  df-fv 6541  df-cring 20375  df-idom 20858

This theorem is used by:  fracfld  33749  dvdsruasso  33818  dvdsruasso2  33819  mxidlirredi  33874  mxidlirred  33875  rprmasso  33935  rprmasso2  33936  unitmulrprm  33938  rprmirred  33941  rprmirredb  33942  1arithidomlem1  33945  1arithidomlem2  33946  1arithidom  33947  pidufd  33953  1arithufdlem2  33955  1arithufdlem4  33957  dfufd2lem  33959  dfufd2  33960  deg1prod  33993  mplidomlem  34037  vietadeg1  34088  vietalem  34089  vieta  34090  assafld  34147  fldextrspunlem1  34185  algextdeglem7  34233  idomnnzpownz  42998  deg1gprod  43006  deg1pow  43007  aks6d1c6lem3  43038  unitscyglem5  43065