Metamath Proof Explorer

Theorem ofldfld

Description: An ordered field is a field. (Contributed by Thierry Arnoux, 20-Jan-2018)

Ref Expression
Assertion ofldfld 
|- ( F e. oField -> F e. Field )

Proof

Step Hyp Ref Expression
1 isofld 
 |-  ( F e. oField <-> ( F e. Field /\ F e. oRing ) )
2 1 simplbi 
 |-  ( F e. oField -> F e. Field )