Theorem idomringd 20811

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

Syntax hints:   → wi 4   ∈ wcel 2149  Ringcrg 20314  IDomncidom 20777

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 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-iota 6493  df-fv 6545  df-cring 20317  df-idom 20780

This theorem is referenced by:  fracfld  33571  dvdsruasso  33641  dvdsruasso2  33642  mxidlirredi  33698  mxidlirred  33699  rprmasso  33759  rprmasso2  33760  unitmulrprm  33762  rprmirred  33765  rprmirredb  33766  1arithidomlem1  33769  1arithidomlem2  33770  1arithidom  33771  pidufd  33777  1arithufdlem2  33779  1arithufdlem4  33781  dfufd2lem  33783  dfufd2  33784  deg1prod  33817  mplidomlem  33861  vietadeg1  33912  vietalem  33913  vieta  33914  assafld  33971  fldextrspunlem1  34009  algextdeglem7  34057  idomnnzpownz  42788  deg1gprod  42796  deg1pow  42797  aks6d1c6lem3  42828  unitscyglem5  42855