Theorem ofldfld

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

	Ref	Expression
Assertion	ofldfld	$$⊢F\in \mathrm{oField}\to F\in \mathrm{Field}$$

Proof

Step	Hyp	Ref	Expression
1		isofld	$$⊢F\in \mathrm{oField}\leftrightarrow \left(F\in \mathrm{Field}\wedge F\in \mathrm{oRing}\right)$$
2	1	simplbi	$$⊢F\in \mathrm{oField}\to F\in \mathrm{Field}$$