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 3438  df-in 3910  df-field 20617

This theorem is referenced by:  resrng  21528  frlmphl  21688  zringfrac  33491  ply1asclunit  33509  ply1unit  33510  ply1dg1rt  33515  ply1dg3rt0irred  33518  fldgenfldext  33635  evls1fldgencl  33637  fldextrspunlsp  33641  irngnzply1lem  33657  irngnzply1  33658  extdgfialglem1  33659  extdgfialglem2  33660  extdgfialg  33661  ply1annig1p  33671  minplycl  33673  ply1annprmidl  33674  minplymindeg  33675  minplyann  33676  minplyirredlem  33677  minplyirred  33678  irngnminplynz  33679  minplym1p  33680  minplynzm1p  33681  minplyelirng  33682  irredminply  33683  algextdeglem1  33684  algextdeglem2  33685  algextdeglem3  33686  algextdeglem4  33687  algextdeglem5  33688  algextdeglem6  33689  algextdeglem7  33690  algextdeglem8  33691  rtelextdg2lem  33693  2sqr3minply  33747  cos9thpiminply  33755  aks6d1c1p3  42083  aks6d1c1p4  42084  aks6d1c1p5  42085  aks6d1c1p7  42086  aks6d1c1p6  42087  aks6d1c1p8  42088  aks6d1c1  42089  aks6d1c2lem3  42099  aks6d1c2lem4  42100  aks6d1c5lem0  42108  aks6d1c5lem1  42109  aks6d1c5lem3  42110  aks6d1c5  42112  aks6d1c6lem1  42143  aks6d1c6lem2  42144  aks6d1c6lem3  42145  aks6d1c6lem4  42146  aks6d1c6lem5  42150  aks5lem1  42159  aks5lem2  42160  aks5lem3a  42162  aks5lem5a  42164  prjcrv0  42606