Theorem fldcrngd 20719

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

Syntax hints:   → wi 4   ∈ wcel 2114  CRingccrg 20215  DivRingcdr 20706  Fieldcfield 20707

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-in 3896  df-field 20709

This theorem is referenced by:  resrng  21601  frlmphl  21761  gsumind  33405  zringfrac  33614  ply1asclunit  33634  ply1unit  33635  ply1dg1rt  33640  ply1dg3rt0irred  33644  psrmonprod  33696  esplyfvaln  33718  fldgenfldext  33812  evls1fldgencl  33814  fldextrspunlsp  33818  irngnzply1lem  33834  irngnzply1  33835  extdgfialglem1  33836  extdgfialglem2  33837  extdgfialg  33838  ply1annig1p  33848  minplycl  33850  ply1annprmidl  33851  minplymindeg  33852  minplyann  33853  minplyirredlem  33854  minplyirred  33855  irngnminplynz  33856  minplym1p  33857  minplynzm1p  33858  minplyelirng  33859  irredminply  33860  algextdeglem1  33861  algextdeglem2  33862  algextdeglem3  33863  algextdeglem4  33864  algextdeglem5  33865  algextdeglem6  33866  algextdeglem7  33867  algextdeglem8  33868  rtelextdg2lem  33870  2sqr3minply  33924  cos9thpiminply  33932  aks6d1c1p3  42549  aks6d1c1p4  42550  aks6d1c1p5  42551  aks6d1c1p7  42552  aks6d1c1p6  42553  aks6d1c1p8  42554  aks6d1c1  42555  aks6d1c2lem3  42565  aks6d1c2lem4  42566  aks6d1c5lem0  42574  aks6d1c5lem1  42575  aks6d1c5lem3  42576  aks6d1c5  42578  aks6d1c6lem1  42609  aks6d1c6lem2  42610  aks6d1c6lem3  42611  aks6d1c6lem4  42612  aks6d1c6lem5  42616  aks5lem1  42625  aks5lem2  42626  aks5lem3a  42628  aks5lem5a  42630  prjcrv0  43066