Theorem fldcrngd 20764

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

Syntax hints:   → wi 4   ∈ wcel 2108  CRingccrg 20261  DivRingcdr 20751  Fieldcfield 20752

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-in 3983  df-field 20754

This theorem is referenced by:  resrng  21662  frlmphl  21824  zringfrac  33547  ply1asclunit  33564  ply1unit  33565  ply1dg1rt  33569  ply1dg3rt0irred  33572  fldgenfldext  33678  evls1fldgencl  33680  irngnzply1lem  33690  irngnzply1  33691  ply1annig1p  33697  minplycl  33699  ply1annprmidl  33700  minplymindeg  33701  minplyann  33702  minplyirredlem  33703  minplyirred  33704  irngnminplynz  33705  minplym1p  33706  irredminply  33707  algextdeglem1  33708  algextdeglem2  33709  algextdeglem3  33710  algextdeglem4  33711  algextdeglem5  33712  algextdeglem6  33713  algextdeglem7  33714  algextdeglem8  33715  rtelextdg2lem  33717  2sqr3minply  33738  aks6d1c1p3  42067  aks6d1c1p4  42068  aks6d1c1p5  42069  aks6d1c1p7  42070  aks6d1c1p6  42071  aks6d1c1p8  42072  aks6d1c1  42073  aks6d1c2lem3  42083  aks6d1c2lem4  42084  aks6d1c5lem0  42092  aks6d1c5lem1  42093  aks6d1c5lem3  42094  aks6d1c5  42096  aks6d1c6lem1  42127  aks6d1c6lem2  42128  aks6d1c6lem3  42129  aks6d1c6lem4  42130  aks6d1c6lem5  42134  aks5lem1  42143  aks5lem2  42144  aks5lem3a  42146  aks5lem5a  42148  prjcrv0  42588