This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem idomringd

Description: An integral domain is a ring. (Contributed by Thierry Arnoux, 22-Mar-2025)

Ref Expression
Hypothesis idomringd.1 ⊢ ( 𝜑 → 𝑅 ∈ IDomn )
Assertion idomringd ( 𝜑 → 𝑅 ∈ Ring )

Proof

Step Hyp Ref Expression
1 idomringd.1 ⊢ ( 𝜑 → 𝑅 ∈ IDomn )
2 1 idomcringd ⊢ ( 𝜑 → 𝑅 ∈ CRing )
3 2 crngringd ⊢ ( 𝜑 → 𝑅 ∈ Ring )