Theorem idomringd 20728

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

Syntax hints:   → wi 4   ∈ wcel 2108  Ringcrg 20230  IDomncidom 20693

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-iota 6514  df-fv 6569  df-cring 20233  df-idom 20696

This theorem is referenced by:  fracfld  33310  dvdsruasso  33413  dvdsruasso2  33414  unitpidl1  33452  mxidlirredi  33499  mxidlirred  33500  rsprprmprmidlb  33551  rprmasso  33553  rprmasso2  33554  unitmulrprm  33556  rprmirred  33559  rprmirredb  33560  1arithidomlem1  33563  1arithidomlem2  33564  1arithidom  33565  pidufd  33571  1arithufdlem2  33573  1arithufdlem4  33575  dfufd2lem  33577  dfufd2  33578  r1pid2OLD  33629  assafld  33688  fldextrspunlem1  33725  algextdeglem7  33764  idomnnzpownz  42133  deg1gprod  42141  deg1pow  42142  aks6d1c6lem3  42173  unitscyglem5  42200