Theorem fldcrngd 20651

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

Syntax hints:   → wi 4   ∈ wcel 2109  CRingccrg 20143  DivRingcdr 20638  Fieldcfield 20639

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-in 3921  df-field 20641

This theorem is referenced by:  resrng  21530  frlmphl  21690  zringfrac  33525  ply1asclunit  33543  ply1unit  33544  ply1dg1rt  33548  ply1dg3rt0irred  33551  fldgenfldext  33663  evls1fldgencl  33665  fldextrspunlsp  33669  irngnzply1lem  33685  irngnzply1  33686  ply1annig1p  33694  minplycl  33696  ply1annprmidl  33697  minplymindeg  33698  minplyann  33699  minplyirredlem  33700  minplyirred  33701  irngnminplynz  33702  minplym1p  33703  minplynzm1p  33704  minplyelirng  33705  irredminply  33706  algextdeglem1  33707  algextdeglem2  33708  algextdeglem3  33709  algextdeglem4  33710  algextdeglem5  33711  algextdeglem6  33712  algextdeglem7  33713  algextdeglem8  33714  rtelextdg2lem  33716  2sqr3minply  33770  cos9thpiminply  33778  aks6d1c1p3  42098  aks6d1c1p4  42099  aks6d1c1p5  42100  aks6d1c1p7  42101  aks6d1c1p6  42102  aks6d1c1p8  42103  aks6d1c1  42104  aks6d1c2lem3  42114  aks6d1c2lem4  42115  aks6d1c5lem0  42123  aks6d1c5lem1  42124  aks6d1c5lem3  42125  aks6d1c5  42127  aks6d1c6lem1  42158  aks6d1c6lem2  42159  aks6d1c6lem3  42160  aks6d1c6lem4  42161  aks6d1c6lem5  42165  aks5lem1  42174  aks5lem2  42175  aks5lem3a  42177  aks5lem5a  42179  prjcrv0  42621