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 
|- ( ph -> R e. IDomn )
Assertion idomringd 
|- ( ph -> R e. Ring )

Proof

Step Hyp Ref Expression
1 idomringd.1 
 |-  ( ph -> R e. IDomn )
2 1 idomcringd 
 |-  ( ph -> R e. CRing )
3 2 crngringd 
 |-  ( ph -> R e. Ring )