Theorem fldcrngd 20687

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

Syntax hints:   → wi 4   ∈ wcel 2114  CRingccrg 20181  DivRingcdr 20674  Fieldcfield 20675

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-in 3910  df-field 20677

This theorem is referenced by:  resrng  21588  frlmphl  21748  gsumind  33438  zringfrac  33647  ply1asclunit  33667  ply1unit  33668  ply1dg1rt  33673  ply1dg3rt0irred  33677  psrmonprod  33729  esplyfvaln  33751  fldgenfldext  33846  evls1fldgencl  33848  fldextrspunlsp  33852  irngnzply1lem  33868  irngnzply1  33869  extdgfialglem1  33870  extdgfialglem2  33871  extdgfialg  33872  ply1annig1p  33882  minplycl  33884  ply1annprmidl  33885  minplymindeg  33886  minplyann  33887  minplyirredlem  33888  minplyirred  33889  irngnminplynz  33890  minplym1p  33891  minplynzm1p  33892  minplyelirng  33893  irredminply  33894  algextdeglem1  33895  algextdeglem2  33896  algextdeglem3  33897  algextdeglem4  33898  algextdeglem5  33899  algextdeglem6  33900  algextdeglem7  33901  algextdeglem8  33902  rtelextdg2lem  33904  2sqr3minply  33958  cos9thpiminply  33966  aks6d1c1p3  42480  aks6d1c1p4  42481  aks6d1c1p5  42482  aks6d1c1p7  42483  aks6d1c1p6  42484  aks6d1c1p8  42485  aks6d1c1  42486  aks6d1c2lem3  42496  aks6d1c2lem4  42497  aks6d1c5lem0  42505  aks6d1c5lem1  42506  aks6d1c5lem3  42507  aks6d1c5  42509  aks6d1c6lem1  42540  aks6d1c6lem2  42541  aks6d1c6lem3  42542  aks6d1c6lem4  42543  aks6d1c6lem5  42547  aks5lem1  42556  aks5lem2  42557  aks5lem3a  42559  aks5lem5a  42561  prjcrv0  42991