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	⊢ ( 𝜑 → 𝑅 ∈ Field )
Assertion	fldcrngd	⊢ ( 𝜑 → 𝑅 ∈ CRing )

Proof

Step	Hyp	Ref	Expression
1		fldcrngd.1	⊢ ( 𝜑 → 𝑅 ∈ Field )
2		isfld	⊢ ( 𝑅 ∈ Field ↔ ( 𝑅 ∈ DivRing ∧ 𝑅 ∈ CRing ) )
3	2	simprbi	⊢ ( 𝑅 ∈ Field → 𝑅 ∈ CRing )
4	1 3	syl	⊢ ( 𝜑 → 𝑅 ∈ CRing )