Theorem fldcrngd 20842

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

Syntax hints:   → wi 4   ∈ wcel 2143  CRingccrg 20311  DivRingcdr 20827  Fieldcfield 20828

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-in 3912  df-field 20830

This theorem is referenced by:  resrng  21771  frlmphl  21931  gsumind  33665  fldlring  33789  zringfrac  33844  ply1asclunit  33864  ply1unit  33865  ply1dg1rt  33870  ply1dg3rt0irred  33874  psrmonprod  33942  esplyfvaln  33964  fldgenfldext  34058  evls1fldgencl  34060  fldextrspunlsp  34064  irngnzply1lem  34080  irngnzply1  34081  extdgfialglem1  34082  extdgfialglem2  34083  extdgfialg  34084  ply1annig1p  34094  minplycl  34096  ply1annprmidl  34097  minplymindeg  34098  minplyann  34099  minplyirredlem  34100  minplyirred  34101  irngnminplynz  34102  minplym1p  34103  minplynzm1p  34104  minplyelirng  34105  irredminply  34106  algextdeglem1  34107  algextdeglem2  34108  algextdeglem3  34109  algextdeglem4  34110  algextdeglem5  34111  algextdeglem6  34112  algextdeglem7  34113  algextdeglem8  34114  rtelextdg2lem  34116  2sqr3minply  34170  cos9thpiminply  34178  aks6d1c1p3  42877  aks6d1c1p4  42878  aks6d1c1p5  42879  aks6d1c1p7  42880  aks6d1c1p6  42881  aks6d1c1p8  42882  aks6d1c1  42883  aks6d1c2lem3  42893  aks6d1c2lem4  42894  aks6d1c5lem0  42902  aks6d1c5lem1  42903  aks6d1c5lem3  42904  aks6d1c5  42906  aks6d1c6lem1  42937  aks6d1c6lem2  42938  aks6d1c6lem3  42939  aks6d1c6lem4  42940  aks6d1c6lem5  42944  aks5lem1  42953  aks5lem2  42954  aks5lem3a  42956  aks5lem5a  42958  prjcrv0  43365