Theorem fldcrngd 20627

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 20625	. . 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 20119  DivRingcdr 20614  Fieldcfield 20615

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 3446  df-in 3918  df-field 20617

This theorem is referenced by:  resrng  21506  frlmphl  21666  zringfrac  33498  ply1asclunit  33516  ply1unit  33517  ply1dg1rt  33521  ply1dg3rt0irred  33524  fldgenfldext  33636  evls1fldgencl  33638  fldextrspunlsp  33642  irngnzply1lem  33658  irngnzply1  33659  ply1annig1p  33667  minplycl  33669  ply1annprmidl  33670  minplymindeg  33671  minplyann  33672  minplyirredlem  33673  minplyirred  33674  irngnminplynz  33675  minplym1p  33676  minplynzm1p  33677  minplyelirng  33678  irredminply  33679  algextdeglem1  33680  algextdeglem2  33681  algextdeglem3  33682  algextdeglem4  33683  algextdeglem5  33684  algextdeglem6  33685  algextdeglem7  33686  algextdeglem8  33687  rtelextdg2lem  33689  2sqr3minply  33743  cos9thpiminply  33751  aks6d1c1p3  42071  aks6d1c1p4  42072  aks6d1c1p5  42073  aks6d1c1p7  42074  aks6d1c1p6  42075  aks6d1c1p8  42076  aks6d1c1  42077  aks6d1c2lem3  42087  aks6d1c2lem4  42088  aks6d1c5lem0  42096  aks6d1c5lem1  42097  aks6d1c5lem3  42098  aks6d1c5  42100  aks6d1c6lem1  42131  aks6d1c6lem2  42132  aks6d1c6lem3  42133  aks6d1c6lem4  42134  aks6d1c6lem5  42138  aks5lem1  42147  aks5lem2  42148  aks5lem3a  42150  aks5lem5a  42152  prjcrv0  42594