Theorem fldcrngd 20892

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 20890	. . 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 20360  DivRingcdr 20877  Fieldcfield 20878

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-in 3913  df-field 20880

This theorem is used by:  resrng  21821  frlmphl  21981  gsumind  33729  fldlring  33853  zringfrac  33908  ply1asclunit  33928  ply1unit  33929  ply1dg1rt  33934  ply1dg3rt0irred  33938  psrmonprod  34006  esplyfvaln  34028  fldgenfldext  34122  evls1fldgencl  34124  fldextrspunlsp  34128  irngnzply1lem  34144  irngnzply1  34145  extdgfialglem1  34146  extdgfialglem2  34147  extdgfialg  34148  ply1annig1p  34158  minplycl  34160  ply1annprmidl  34161  minplymindeg  34162  minplyann  34163  minplyirredlem  34164  minplyirred  34165  irngnminplynz  34166  minplym1p  34167  minplynzm1p  34168  minplyelirng  34169  irredminply  34170  algextdeglem1  34171  algextdeglem2  34172  algextdeglem3  34173  algextdeglem4  34174  algextdeglem5  34175  algextdeglem6  34176  algextdeglem7  34177  algextdeglem8  34178  rtelextdg2lem  34180  2sqr3minply  34234  cos9thpiminply  34242  aks6d1c1p3  42935  aks6d1c1p4  42936  aks6d1c1p5  42937  aks6d1c1p7  42938  aks6d1c1p6  42939  aks6d1c1p8  42940  aks6d1c1  42941  aks6d1c2lem3  42951  aks6d1c2lem4  42952  aks6d1c5lem0  42960  aks6d1c5lem1  42961  aks6d1c5lem3  42962  aks6d1c5  42964  aks6d1c6lem1  42995  aks6d1c6lem2  42996  aks6d1c6lem3  42997  aks6d1c6lem4  42998  aks6d1c6lem5  43002  aks5lem1  43011  aks5lem2  43012  aks5lem3a  43014  aks5lem5a  43016  prjcrv0  43423