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

Proof

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