Theorem idomringd 20750

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

Syntax hints:   → wi 4   ∈ wcel 2108  Ringcrg 20260  IDomncidom 20715

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-iota 6525  df-fv 6581  df-cring 20263  df-idom 20718

This theorem is referenced by:  fracfld  33275  dvdsruasso  33378  dvdsruasso2  33379  unitpidl1  33417  mxidlirredi  33464  mxidlirred  33465  rsprprmprmidlb  33516  rprmasso  33518  rprmasso2  33519  unitmulrprm  33521  rprmirred  33524  rprmirredb  33525  1arithidomlem1  33528  1arithidomlem2  33529  1arithidom  33530  pidufd  33536  1arithufdlem2  33538  1arithufdlem4  33540  dfufd2lem  33542  dfufd2  33543  r1pid2OLD  33594  assafld  33650  algextdeglem7  33714  idomnnzpownz  42089  deg1gprod  42097  deg1pow  42098  aks6d1c6lem3  42129  unitscyglem5  42156