Theorem fldcrngd 20657

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

Syntax hints:   → wi 4   ∈ wcel 2111  CRingccrg 20152  DivRingcdr 20644  Fieldcfield 20645

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 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-in 3904  df-field 20647

This theorem is referenced by:  resrng  21558  frlmphl  21718  gsumind  33310  zringfrac  33519  ply1asclunit  33537  ply1unit  33538  ply1dg1rt  33543  ply1dg3rt0irred  33546  fldgenfldext  33681  evls1fldgencl  33683  fldextrspunlsp  33687  irngnzply1lem  33703  irngnzply1  33704  extdgfialglem1  33705  extdgfialglem2  33706  extdgfialg  33707  ply1annig1p  33717  minplycl  33719  ply1annprmidl  33720  minplymindeg  33721  minplyann  33722  minplyirredlem  33723  minplyirred  33724  irngnminplynz  33725  minplym1p  33726  minplynzm1p  33727  minplyelirng  33728  irredminply  33729  algextdeglem1  33730  algextdeglem2  33731  algextdeglem3  33732  algextdeglem4  33733  algextdeglem5  33734  algextdeglem6  33735  algextdeglem7  33736  algextdeglem8  33737  rtelextdg2lem  33739  2sqr3minply  33793  cos9thpiminply  33801  aks6d1c1p3  42213  aks6d1c1p4  42214  aks6d1c1p5  42215  aks6d1c1p7  42216  aks6d1c1p6  42217  aks6d1c1p8  42218  aks6d1c1  42219  aks6d1c2lem3  42229  aks6d1c2lem4  42230  aks6d1c5lem0  42238  aks6d1c5lem1  42239  aks6d1c5lem3  42240  aks6d1c5  42242  aks6d1c6lem1  42273  aks6d1c6lem2  42274  aks6d1c6lem3  42275  aks6d1c6lem4  42276  aks6d1c6lem5  42280  aks5lem1  42289  aks5lem2  42290  aks5lem3a  42292  aks5lem5a  42294  prjcrv0  42736