Theorem idomringd 20638

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

Syntax hints:   → wi 4   ∈ wcel 2111  Ringcrg 20146  IDomncidom 20603

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4279  df-if 4471  df-sn 4572  df-pr 4574  df-op 4578  df-uni 4855  df-br 5087  df-iota 6432  df-fv 6484  df-cring 20149  df-idom 20606

This theorem is referenced by:  fracfld  33266  dvdsruasso  33342  dvdsruasso2  33343  unitpidl1  33381  mxidlirredi  33428  mxidlirred  33429  rsprprmprmidlb  33480  rprmasso  33482  rprmasso2  33483  unitmulrprm  33485  rprmirred  33488  rprmirredb  33489  1arithidomlem1  33492  1arithidomlem2  33493  1arithidom  33494  pidufd  33500  1arithufdlem2  33502  1arithufdlem4  33504  dfufd2lem  33506  dfufd2  33507  r1pid2OLD  33561  assafld  33642  fldextrspunlem1  33680  algextdeglem7  33728  idomnnzpownz  42165  deg1gprod  42173  deg1pow  42174  aks6d1c6lem3  42205  unitscyglem5  42232