Theorem fldcrngd 20374

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

Hypothesis

Ref	Expression
fldcrngd.1	⊢ (𝜑 → 𝑅 ∈ Field)

Assertion

Ref	Expression
fldcrngd	⊢ (𝜑 → 𝑅 ∈ CRing)

Proof of Theorem fldcrngd

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

Syntax hints:   → wi 4   ∈ wcel 2106  CRingccrg 20059  DivRingcdr 20361  Fieldcfield 20362

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-in 3955  df-field 20364

This theorem is referenced by:  resrng  21180  frlmphl  21342  ply1asclunit  32699  evls1fldgencl  32804  irngnzply1lem  32814  irngnzply1  32815  ply1annig1p  32825  minplycl  32827  ply1annprmidl  32828  minplyirredlem  32829  minplyirred  32830  irngnminplynz  32831  minplym1p  32832  algextdeglem1  32833  algextdeglem2  32834  algextdeglem3  32835  algextdeglem4  32836  algextdeglem5  32837  algextdeglem6  32838  algextdeglem7  32839  algextdeglem8  32840  prjcrv0  41457