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 )