Theorem fldcrngd

Description: A field is a commutative ring. (Contributed by Jeff Madsen, 8-Jun-2010) (Revised by SN, 23-Nov-2024)

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

Proof

Step	Hyp	Ref	Expression
1		fldcrngd.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	simprbi	$$⊢R\in \mathrm{Field}\to R\in \mathrm{CRing}$$
4	1 3	syl	$$⊢\phi \to R\in \mathrm{CRing}$$