MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  crngringd Structured version   Visualization version   GIF version

Theorem crngringd 19985
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
StepHypRef Expression
1 crngringd.1 . 2 (𝜑𝑅 ∈ CRing)
2 crngring 19984 . 2 (𝑅 ∈ CRing → 𝑅 ∈ Ring)
31, 2syl 17 1 (𝜑𝑅 ∈ Ring)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107  Ringcrg 19972  CRingccrg 19973
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3407  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4287  df-if 4491  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4870  df-br 5110  df-iota 6452  df-fv 6508  df-cring 19975
This theorem is referenced by:  crnggrpd  19986  asclrhm  21316  evlslem1  21515  recvs  24532  frobrhm  32124  fermltlchr  32208  znfermltl  32209  idlsrgmulrssin  32310  evls1expd  32325  evls1fpws  32327  ressply1evl  32328  ply1fermltlchr  32339  elirng  32424  0ringirng  32427  irngnzply1lem  32428  evls1maprhm  32432  ply1annidl  32434  zarclsun  32515  zarmxt1  32525  zarcmplem  32526  fldhmf1  40597  riccrng1  40752  pwsgprod  40779  mplascl0  40789  evl0  40790  evlsval3  40791  evlsbagval  40795  evlsexpval  40796  evlsevl  40799  selvmul  40811  mhphf  40818  mhphf4  40821
  Copyright terms: Public domain W3C validator