Theorem idomringd 20972

Description: An integral domain is a ring. (Contributed by Jeff Madsen, 6-Jan-2011.) (Revised 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 20971	. 2 ⊢ (𝜑 → 𝑅 ∈ CRing)
3	2	crngringd 20466	1 ⊢ (𝜑 → 𝑅 ∈ Ring)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  Ringcrg 20452  IDomncidom 20938

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 2733

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 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  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 6493  df-fv 6545  df-cring 20455  df-idom 20941

This theorem is used by:  fracfld  33863  dvdsruasso  33933  dvdsruasso2  33934  mxidlirredi  33989  mxidlirred  33990  rprmasso  34050  rprmasso2  34051  unitmulrprm  34053  rprmirred  34056  rprmirredb  34057  1arithidomlem1  34060  1arithidomlem2  34061  1arithidom  34062  pidufd  34068  1arithufdlem2  34070  1arithufdlem4  34072  dfufd2lem  34074  dfufd2  34075  deg1prod  34108  mplidomlem  34152  vietadeg1  34203  vietalem  34204  vieta  34205  assafld  34262  fldextrspunlem1  34300  algextdeglem7  34348  idomnnzpownz  43162  deg1gprod  43170  deg1pow  43171  aks6d1c6lem3  43202  unitscyglem5  43229