Theorem fldcrngd 20662

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 20660	. . 3 ⊢ (𝑅 ∈ Field ↔ (𝑅 ∈ DivRing ∧ 𝑅 ∈ CRing))
3	2	simprbi 496	. 2 ⊢ (𝑅 ∈ Field → 𝑅 ∈ CRing)
4	1, 3	syl 17	1 ⊢ (𝜑 → 𝑅 ∈ CRing)

Syntax hints:   → wi 4   ∈ wcel 2109  CRingccrg 20154  DivRingcdr 20649  Fieldcfield 20650

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3446  df-in 3918  df-field 20652

This theorem is referenced by:  resrng  21563  frlmphl  21723  zringfrac  33518  ply1asclunit  33536  ply1unit  33537  ply1dg1rt  33541  ply1dg3rt0irred  33544  fldgenfldext  33656  evls1fldgencl  33658  fldextrspunlsp  33662  irngnzply1lem  33678  irngnzply1  33679  ply1annig1p  33687  minplycl  33689  ply1annprmidl  33690  minplymindeg  33691  minplyann  33692  minplyirredlem  33693  minplyirred  33694  irngnminplynz  33695  minplym1p  33696  minplynzm1p  33697  minplyelirng  33698  irredminply  33699  algextdeglem1  33700  algextdeglem2  33701  algextdeglem3  33702  algextdeglem4  33703  algextdeglem5  33704  algextdeglem6  33705  algextdeglem7  33706  algextdeglem8  33707  rtelextdg2lem  33709  2sqr3minply  33763  cos9thpiminply  33771  aks6d1c1p3  42091  aks6d1c1p4  42092  aks6d1c1p5  42093  aks6d1c1p7  42094  aks6d1c1p6  42095  aks6d1c1p8  42096  aks6d1c1  42097  aks6d1c2lem3  42107  aks6d1c2lem4  42108  aks6d1c5lem0  42116  aks6d1c5lem1  42117  aks6d1c5lem3  42118  aks6d1c5  42120  aks6d1c6lem1  42151  aks6d1c6lem2  42152  aks6d1c6lem3  42153  aks6d1c6lem4  42154  aks6d1c6lem5  42158  aks5lem1  42167  aks5lem2  42168  aks5lem3a  42170  aks5lem5a  42172  prjcrv0  42614