Metamath Proof Explorer

Theorem fldcrngd

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

Ref Expression
Hypothesis fldcrngd.1 
|- ( ph -> R e. Field )
Assertion fldcrngd 
|- ( ph -> R e. CRing )

Proof

Step Hyp Ref Expression
1 fldcrngd.1 
 |-  ( ph -> R e. Field )
2 isfld 
 |-  ( R e. Field <-> ( R e. DivRing /\ R e. CRing ) )
3 2 simprbi 
 |-  ( R e. Field -> R e. CRing )
4 1 3 syl 
 |-  ( ph -> R e. CRing )