Theorem fldcrngd 20675

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

Syntax hints:   → wi 4   ∈ wcel 2113  CRingccrg 20169  DivRingcdr 20662  Fieldcfield 20663

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-in 3908  df-field 20665

This theorem is referenced by:  resrng  21576  frlmphl  21736  gsumind  33426  zringfrac  33635  ply1asclunit  33655  ply1unit  33656  ply1dg1rt  33661  ply1dg3rt0irred  33665  fldgenfldext  33825  evls1fldgencl  33827  fldextrspunlsp  33831  irngnzply1lem  33847  irngnzply1  33848  extdgfialglem1  33849  extdgfialglem2  33850  extdgfialg  33851  ply1annig1p  33861  minplycl  33863  ply1annprmidl  33864  minplymindeg  33865  minplyann  33866  minplyirredlem  33867  minplyirred  33868  irngnminplynz  33869  minplym1p  33870  minplynzm1p  33871  minplyelirng  33872  irredminply  33873  algextdeglem1  33874  algextdeglem2  33875  algextdeglem3  33876  algextdeglem4  33877  algextdeglem5  33878  algextdeglem6  33879  algextdeglem7  33880  algextdeglem8  33881  rtelextdg2lem  33883  2sqr3minply  33937  cos9thpiminply  33945  aks6d1c1p3  42364  aks6d1c1p4  42365  aks6d1c1p5  42366  aks6d1c1p7  42367  aks6d1c1p6  42368  aks6d1c1p8  42369  aks6d1c1  42370  aks6d1c2lem3  42380  aks6d1c2lem4  42381  aks6d1c5lem0  42389  aks6d1c5lem1  42390  aks6d1c5lem3  42391  aks6d1c5  42393  aks6d1c6lem1  42424  aks6d1c6lem2  42425  aks6d1c6lem3  42426  aks6d1c6lem4  42427  aks6d1c6lem5  42431  aks5lem1  42440  aks5lem2  42441  aks5lem3a  42443  aks5lem5a  42445  prjcrv0  42876