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

Metamath Proof Explorer

Theorem ofldfld

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

Ref Expression
Assertion ofldfld ( 𝐹 ∈ oField → 𝐹 ∈ Field )

Proof

Step Hyp Ref Expression
1 isofld ⊢ ( 𝐹 ∈ oField ↔ ( 𝐹 ∈ Field ∧ 𝐹 ∈ oRing ) )
2 1 simplbi ⊢ ( 𝐹 ∈ oField → 𝐹 ∈ Field )