Theorem idomringd 20705

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

Syntax hints:   → wi 4   ∈ wcel 2114  Ringcrg 20214  IDomncidom 20670

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-iota 6454  df-fv 6506  df-cring 20217  df-idom 20673

This theorem is referenced by:  fracfld  33369  dvdsruasso  33445  dvdsruasso2  33446  unitpidl1  33484  mxidlirredi  33531  mxidlirred  33532  rsprprmprmidlb  33583  rprmasso  33585  rprmasso2  33586  unitmulrprm  33588  rprmirred  33591  rprmirredb  33592  1arithidomlem1  33595  1arithidomlem2  33596  1arithidom  33597  pidufd  33603  1arithufdlem2  33605  1arithufdlem4  33607  dfufd2lem  33609  dfufd2  33610  deg1prod  33643  r1pid2OLD  33669  vietadeg1  33722  vietalem  33723  vieta  33724  assafld  33781  fldextrspunlem1  33819  algextdeglem7  33867  idomnnzpownz  42571  deg1gprod  42579  deg1pow  42580  aks6d1c6lem3  42611  unitscyglem5  42638