Theorem fldcrngd 20792

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

Syntax hints:   → wi 4   ∈ wcel 2142  CRingccrg 20284  DivRingcdr 20779  Fieldcfield 20780

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-in 3911  df-field 20782

This theorem is referenced by:  resrng  21673  frlmphl  21833  gsumind  33531  fldlring  33695  zringfrac  33750  ply1asclunit  33770  ply1unit  33771  ply1dg1rt  33776  ply1dg3rt0irred  33780  psrmonprod  33849  esplyfvaln  33871  fldgenfldext  33965  evls1fldgencl  33967  fldextrspunlsp  33971  irngnzply1lem  33987  irngnzply1  33988  extdgfialglem1  33989  extdgfialglem2  33990  extdgfialg  33991  ply1annig1p  34001  minplycl  34003  ply1annprmidl  34004  minplymindeg  34005  minplyann  34006  minplyirredlem  34007  minplyirred  34008  irngnminplynz  34009  minplym1p  34010  minplynzm1p  34011  minplyelirng  34012  irredminply  34013  algextdeglem1  34014  algextdeglem2  34015  algextdeglem3  34016  algextdeglem4  34017  algextdeglem5  34018  algextdeglem6  34019  algextdeglem7  34020  algextdeglem8  34021  rtelextdg2lem  34023  2sqr3minply  34077  cos9thpiminply  34085  aks6d1c1p3  42727  aks6d1c1p4  42728  aks6d1c1p5  42729  aks6d1c1p7  42730  aks6d1c1p6  42731  aks6d1c1p8  42732  aks6d1c1  42733  aks6d1c2lem3  42743  aks6d1c2lem4  42744  aks6d1c5lem0  42752  aks6d1c5lem1  42753  aks6d1c5lem3  42754  aks6d1c5  42756  aks6d1c6lem1  42787  aks6d1c6lem2  42788  aks6d1c6lem3  42789  aks6d1c6lem4  42790  aks6d1c6lem5  42794  aks5lem1  42803  aks5lem2  42804  aks5lem3a  42806  aks5lem5a  42808  prjcrv0  43215