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

Metamath Proof Explorer

Theorem fldcrngd

Description: A field is a commutative ring. (Contributed by SN, 23-Nov-2024)

		Ref	Expression
	Hypothesis	fldcrngd.1	$⊢ φ \to R \in Field$
	Assertion	fldcrngd	$⊢ φ \to R \in CRing$

Step	Hyp	Ref	Expression
1		fldcrngd.1	$⊢ φ \to R \in Field$
2		isfld	$⊢ R \in Field \leftrightarrow (R \in DivRing \land R \in CRing)$
3	2	simprbi	$⊢ R \in Field \to R \in CRing$
4	1 3	syl	$⊢ φ \to R \in CRing$