Metamath Proof Explorer


Theorem flddrngd

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

Ref Expression
Hypothesis flddrngd.1 φ R Field
Assertion flddrngd φ R DivRing

Proof

Step Hyp Ref Expression
1 flddrngd.1 φ R Field
2 isfld R Field R DivRing R CRing
3 2 simplbi R Field R DivRing
4 1 3 syl φ R DivRing