Metamath Proof Explorer

Theorem flddrngd

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

Ref Expression
Hypothesis flddrngd.1 
|- ( ph -> R e. Field )
Assertion flddrngd 
|- ( ph -> R e. DivRing )

Proof

Step Hyp Ref Expression
1 flddrngd.1 
 |-  ( ph -> R e. Field )
2 isfld 
 |-  ( R e. Field <-> ( R e. DivRing /\ R e. CRing ) )
3 2 simplbi 
 |-  ( R e. Field -> R e. DivRing )
4 1 3 syl 
 |-  ( ph -> R e. DivRing )