Theorem fldcrngd

Description: A field is a commutative ring. EDITORIAL: Shortens recrng . Also recrng should be named resrng. Also fldcrng is misnamed. (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 )