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

Theorem nzrring 19475
Description: A nonzero ring is a ring. (Contributed by Stefan O'Rear, 24-Feb-2015.)
Assertion
Ref Expression
nzrring (𝑅 ∈ NzRing → 𝑅 ∈ Ring)

Proof of Theorem nzrring
StepHypRef Expression
1 eqid 2770 . . 3 (1r𝑅) = (1r𝑅)
2 eqid 2770 . . 3 (0g𝑅) = (0g𝑅)
31, 2isnzr 19473 . 2 (𝑅 ∈ NzRing ↔ (𝑅 ∈ Ring ∧ (1r𝑅) ≠ (0g𝑅)))
43simplbi 479 1 (𝑅 ∈ NzRing → 𝑅 ∈ Ring)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2144  wne 2942  cfv 6031  0gc0g 16307  1rcur 18708  Ringcrg 18754  NzRingcnzr 19471
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-13 2407  ax-ext 2750
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-3an 1072  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-clab 2757  df-cleq 2763  df-clel 2766  df-nfc 2901  df-ne 2943  df-rex 3066  df-rab 3069  df-v 3351  df-dif 3724  df-un 3726  df-in 3728  df-ss 3735  df-nul 4062  df-if 4224  df-sn 4315  df-pr 4317  df-op 4321  df-uni 4573  df-br 4785  df-iota 5994  df-fv 6039  df-nzr 19472
This theorem is referenced by:  opprnzr  19479  nzrunit  19481  domnring  19510  domnchr  20094  uvcf1  20347  lindfind2  20373  frlmisfrlm  20403  nminvr  22692  deg1pw  24099  ply1nz  24100  ply1remlem  24141  ply1rem  24142  facth1  24143  fta1glem1  24144  fta1glem2  24145  zrhnm  30347  mon1pid  38302  mon1psubm  38303  nzrneg1ne0  42387  islindeps2  42790
  Copyright terms: Public domain W3C validator