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

Metamath Proof Explorer

Theorem subrfld

Description: A subring of a field is an integral domain. (Contributed by Thierry Arnoux, 18-May-2025)

Ref Expression
Hypotheses subrfld.1 ⊢ φ → R ∈ Field
subrfld.2 ⊢ φ → S ∈ SubRing ⁡ R
Assertion subrfld ⊢ φ → R ↾ 𝑠 S ∈ IDomn

Proof

Step Hyp Ref Expression
1 subrfld.1 ⊢ φ → R ∈ Field
2 subrfld.2 ⊢ φ → S ∈ SubRing ⁡ R
3 fldidom ⊢ R ∈ Field → R ∈ IDomn
4 1 3 syl ⊢ φ → R ∈ IDomn
5 4 2 subridom ⊢ φ → R ↾ 𝑠 S ∈ IDomn