Theorem fldcrngd 21007

Description: A field is a commutative ring. (Contributed by Jeff Madsen, 8-Jun-2010.) (Revised 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 21005	. . 3 ⊢ (𝑅 ∈ Field ↔ (𝑅 ∈ DivRing ∧ 𝑅 ∈ CRing))
3	2	simprbi 503	. 2 ⊢ (𝑅 ∈ Field → 𝑅 ∈ CRing)
4	1, 3	syl 18	1 ⊢ (𝜑 → 𝑅 ∈ CRing)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  CRingccrg 20472  DivRingcdr 20992  Fieldcfield 20993

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3455  df-in 4093  df-field 20995

This theorem is used by:  resrng  21939  frlmphl  22099  gsumind  33959  fldlring  34084  zringfrac  34139  ply1asclunit  34159  ply1unit  34160  ply1dg1rt  34165  ply1dg3rt0irred  34169  psrmonprod  34237  esplyfvaln  34259  fldgenfldext  34353  evls1fldgencl  34355  fldextrspunlsp  34359  irngnzply1lem  34375  irngnzply1  34376  extdgfialglem1  34377  extdgfialglem2  34378  extdgfialg  34379  ply1annig1p  34389  minplycl  34391  ply1annprmidl  34392  minplymindeg  34393  minplyann  34394  minplyirredlem  34395  minplyirred  34396  irngnminplynz  34397  minplym1p  34398  minplynzm1p  34399  minplyelirng  34400  irredminply  34401  algextdeglem1  34402  algextdeglem2  34403  algextdeglem3  34404  algextdeglem4  34405  algextdeglem5  34406  algextdeglem6  34407  algextdeglem7  34408  algextdeglem8  34409  rtelextdg2lem  34411  2sqr3minply  34465  cos9thpiminply  34473  aks6d1c1p3  43300  aks6d1c1p4  43301  aks6d1c1p5  43302  aks6d1c1p7  43303  aks6d1c1p6  43304  aks6d1c1p8  43305  aks6d1c1  43306  aks6d1c2lem3  43316  aks6d1c2lem4  43317  aks6d1c5lem0  43325  aks6d1c5lem1  43326  aks6d1c5lem3  43327  aks6d1c5  43329  aks6d1c6lem1  43360  aks6d1c6lem2  43361  aks6d1c6lem3  43362  aks6d1c6lem4  43363  aks6d1c6lem5  43367  aks5lem1  43376  aks5lem2  43377  aks5lem3a  43379  aks5lem5a  43381  prjcrv0  43809