Metamath Proof Explorer


Theorem fldcrngd

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

Ref Expression
Hypothesis fldcrngd.1 φ R Field
Assertion fldcrngd φ R CRing

Proof

Step Hyp Ref Expression
1 fldcrngd.1 φ R Field
2 isfld R Field R DivRing R CRing
3 2 simprbi R Field R CRing
4 1 3 syl φ R CRing