Theorem fldcrngd 21046

Description: A field is a commutative ring. (Contributed by Jeff Madsen, 8-Jun-2010.) (Revised 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 21044	. . 3 ⊢ (𝑅 ∈ Field ↔ (𝑅 ∈ DivRing ∧ 𝑅 ∈ CRing))
3	2	simprbi 503	. 2 ⊢ (𝑅 ∈ Field → 𝑅 ∈ CRing)
4	1, 3	syl 18	1 ⊢ (𝜑 → 𝑅 ∈ CRing)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  CRingccrg 20511  DivRingcdr 21031  Fieldcfield 21032

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-in 4094  df-field 21034

This theorem is used by:  resrng  21982  frlmphl  22142  gsumind  34010  fldlring  34135  zringfrac  34189  ply1asclunit  34209  ply1unit  34210  ply1dg1rt  34215  ply1dg3rt0irred  34219  psrmonprod  34295  esplyfvaln  34317  fldgenfldext  34411  evls1fldgencl  34413  fldextrspunlsp  34417  irngnzply1lem  34433  irngnzply1  34434  extdgfialglem1  34435  extdgfialglem2  34436  extdgfialg  34437  ply1annig1p  34447  minplycl  34449  ply1annprmidl  34450  minplymindeg  34451  minplyann  34452  minplyirredlem  34453  minplyirred  34454  irngnminplynz  34455  minplym1p  34456  minplynzm1p  34457  minplyelirng  34458  irredminply  34459  algextdeglem1  34460  algextdeglem2  34461  algextdeglem3  34462  algextdeglem4  34463  algextdeglem5  34464  algextdeglem6  34465  algextdeglem7  34466  algextdeglem8  34467  rtelextdg2lem  34469  2sqr3minply  34523  cos9thpiminply  34531  aks6d1c1p3  43426  aks6d1c1p4  43427  aks6d1c1p5  43428  aks6d1c1p7  43429  aks6d1c1p6  43430  aks6d1c1p8  43431  aks6d1c1  43432  aks6d1c2lem3  43442  aks6d1c2lem4  43443  aks6d1c5lem0  43451  aks6d1c5lem1  43452  aks6d1c5lem3  43453  aks6d1c5  43455  aks6d1c6lem1  43486  aks6d1c6lem2  43487  aks6d1c6lem3  43488  aks6d1c6lem4  43489  aks6d1c6lem5  43493  aks5lem1  43502  aks5lem2  43503  aks5lem3a  43505  aks5lem5a  43507  prjcrv0  43935