Theorem idomringd 20808

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

Syntax hints:   → wi 4   ∈ wcel 2149  Ringcrg 20311  IDomncidom 20774

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-br 5111  df-iota 6490  df-fv 6542  df-cring 20314  df-idom 20777

This theorem is referenced by:  fracfld  33568  dvdsruasso  33638  dvdsruasso2  33639  mxidlirredi  33695  mxidlirred  33696  rprmasso  33756  rprmasso2  33757  unitmulrprm  33759  rprmirred  33762  rprmirredb  33763  1arithidomlem1  33766  1arithidomlem2  33767  1arithidom  33768  pidufd  33774  1arithufdlem2  33776  1arithufdlem4  33778  dfufd2lem  33780  dfufd2  33781  deg1prod  33814  mplidomlem  33858  vietadeg1  33909  vietalem  33910  vieta  33911  assafld  33968  fldextrspunlem1  34006  algextdeglem7  34054  idomnnzpownz  42784  deg1gprod  42792  deg1pow  42793  aks6d1c6lem3  42824  unitscyglem5  42851