Theorem fldcrngd 20995

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 20993	. . 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 2145  CRingccrg 20460  DivRingcdr 20980  Fieldcfield 20981

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 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-in 3906  df-field 20983

This theorem is used by:  resrng  21927  frlmphl  22087  gsumind  33906  fldlring  34031  zringfrac  34086  ply1asclunit  34106  ply1unit  34107  ply1dg1rt  34112  ply1dg3rt0irred  34116  psrmonprod  34184  esplyfvaln  34206  fldgenfldext  34300  evls1fldgencl  34302  fldextrspunlsp  34306  irngnzply1lem  34322  irngnzply1  34323  extdgfialglem1  34324  extdgfialglem2  34325  extdgfialg  34326  ply1annig1p  34336  minplycl  34338  ply1annprmidl  34339  minplymindeg  34340  minplyann  34341  minplyirredlem  34342  minplyirred  34343  irngnminplynz  34344  minplym1p  34345  minplynzm1p  34346  minplyelirng  34347  irredminply  34348  algextdeglem1  34349  algextdeglem2  34350  algextdeglem3  34351  algextdeglem4  34352  algextdeglem5  34353  algextdeglem6  34354  algextdeglem7  34355  algextdeglem8  34356  rtelextdg2lem  34358  2sqr3minply  34412  cos9thpiminply  34420  aks6d1c1p3  43160  aks6d1c1p4  43161  aks6d1c1p5  43162  aks6d1c1p7  43163  aks6d1c1p6  43164  aks6d1c1p8  43165  aks6d1c1  43166  aks6d1c2lem3  43176  aks6d1c2lem4  43177  aks6d1c5lem0  43185  aks6d1c5lem1  43186  aks6d1c5lem3  43187  aks6d1c5  43189  aks6d1c6lem1  43220  aks6d1c6lem2  43221  aks6d1c6lem3  43222  aks6d1c6lem4  43223  aks6d1c6lem5  43227  aks5lem1  43236  aks5lem2  43237  aks5lem3a  43239  aks5lem5a  43241  prjcrv0  43669