Theorem crngringd 20204

Description: A commutative ring is a ring. (Contributed by SN, 16-May-2024.)

Hypothesis

Ref	Expression
crngringd.1	⊢ (𝜑 → 𝑅 ∈ CRing)

Assertion

Ref	Expression
crngringd	⊢ (𝜑 → 𝑅 ∈ Ring)

Proof of Theorem crngringd

Step	Hyp	Ref	Expression
1		crngringd.1	. 2 ⊢ (𝜑 → 𝑅 ∈ CRing)
2		crngring 20203	. 2 ⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring)
3	1, 2	syl 17	1 ⊢ (𝜑 → 𝑅 ∈ Ring)

Syntax hints:   → wi 4   ∈ wcel 2108  Ringcrg 20191  CRingccrg 20192

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-iota 6483  df-fv 6538  df-cring 20194

This theorem is referenced by:  crnggrpd  20205  crng12d  20216  crng32d  20217  idomringd  20686  qusmulcrng  21243  rhmqusnsg  21244  fermltlchr  21488  frobrhm  21534  psrassa  21931  evlslem1  22038  psdvsca  22100  psdmul  22102  psd1  22103  psdascl  22104  psdpw  22106  ply1fermltlchr  22248  evls1expd  22303  evls1fpws  22305  ressply1evl  22306  evls1maprhm  22312  evl1maprhm  22315  mdetrsca  22539  recvs  25095  elrgspnsubrunlem1  33188  elrgspnsubrunlem2  33189  elrgspnsubrun  33190  erlbr2d  33205  erler  33206  rlocaddval  33209  rlocmulval  33210  rloccring  33211  rloc0g  33212  rloc1r  33213  rlocf1  33214  fracerl  33246  fracf1  33247  fracfld  33248  znfermltl  33327  ssdifidlprm  33419  mxidlprmALT  33460  idlsrgmulrssin  33474  rsprprmprmidl  33483  rprmndvdsru  33490  rprmirredlem  33491  rprmdvdspow  33494  rprmdvdsprod  33495  1arithufdlem3  33507  zringfrac  33515  evl1fpws  33523  ressply1evls1  33524  ressasclcl  33530  ply1unit  33534  evl1deg1  33535  evl1deg2  33536  evl1deg3  33537  ply1dg1rt  33538  ply1mulrtss  33540  ply1dg3rt0irred  33541  vr1nz  33549  fldgenfldext  33655  evls1fldgencl  33657  fldextrspunlsp  33661  elirng  33673  0ringirng  33676  irngnzply1lem  33677  ply1annidl  33682  ply1annnr  33683  irredminply  33696  algextdeglem4  33700  rtelextdg2lem  33706  cos9thpiminply  33768  zarclsun  33847  zarmxt1  33857  zarcmplem  33858  zndvdchrrhm  41931  fldhmf1  42049  aks6d1c1p2  42068  aks6d1c1p3  42069  aks6d1c1p4  42070  evl1gprodd  42076  aks6d1c2lem4  42086  aks6d1c5lem0  42094  aks6d1c5lem2  42097  aks6d1c5  42098  aks6d1c6lem2  42130  rhmqusspan  42144  aks5lem2  42146  ply1asclzrhval  42147  aks5lem3a  42148  aks5lem5a  42150  riccrng1  42491  pwsgprod  42514  evl0  42527  evlsval3  42529  evlsvvvallem  42531  evlsvvvallem2  42532  evlsvvval  42533  evlsbagval  42536  evlsexpval  42537  evlsmaprhm  42540  evlsevl  42541  evlvvval  42543  evlvvvallem  42544  selvcllem5  42552  selvvvval  42555  evlselv  42557  selvmul  42559  evlsmhpvvval  42565  mhphf  42567  mhphf4  42570