Theorem flddrngd

Description: A field is a division ring. (Contributed by Jeff Madsen, 10-Jun-2010) (Revised by SN, 17-Jan-2025)

	Ref	Expression
Hypothesis	flddrngd.1	$$⊢\phi \to R\in \mathrm{Field}$$
Assertion	flddrngd	$$⊢\phi \to R\in \mathrm{DivRing}$$

Proof

Step	Hyp	Ref	Expression
1		flddrngd.1	$$⊢\phi \to R\in \mathrm{Field}$$
2		isfld	$$⊢R\in \mathrm{Field}\leftrightarrow \left(R\in \mathrm{DivRing}\wedge R\in \mathrm{CRing}\right)$$
3	2	simplbi	$$⊢R\in \mathrm{Field}\to R\in \mathrm{DivRing}$$
4	1 3	syl	$$⊢\phi \to R\in \mathrm{DivRing}$$