Metamath Proof Explorer


Theorem flddrngd

Description: A field is a division ring. (Contributed by SN, 17-Jan-2025)

Ref Expression
Hypothesis flddrngd.1 ( 𝜑𝑅 ∈ Field )
Assertion flddrngd ( 𝜑𝑅 ∈ DivRing )

Proof

Step Hyp Ref Expression
1 flddrngd.1 ( 𝜑𝑅 ∈ Field )
2 isfld ( 𝑅 ∈ Field ↔ ( 𝑅 ∈ DivRing ∧ 𝑅 ∈ CRing ) )
3 2 simplbi ( 𝑅 ∈ Field → 𝑅 ∈ DivRing )
4 1 3 syl ( 𝜑𝑅 ∈ DivRing )