Theorem nzrring 20532

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

Step	Hyp	Ref	Expression
1		eqid 2738	. . 3 ⊢ (1r‘𝑅) = (1r‘𝑅)
2		eqid 2738	. . 3 ⊢ (0g‘𝑅) = (0g‘𝑅)
3	1, 2	isnzr 20530	. 2 ⊢ (𝑅 ∈ NzRing ↔ (𝑅 ∈ Ring ∧ (1r‘𝑅) ≠ (0g‘𝑅)))
4	3	simplbi 498	1 ⊢ (𝑅 ∈ NzRing → 𝑅 ∈ Ring)

Syntax hints:   → wi 4   ∈ wcel 2106   ≠ wne 2943  ‘cfv 6433  0_gc0g 17150  1_rcur 19737  Ringcrg 19783  NzRingcnzr 20528

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ne 2944  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-iota 6391  df-fv 6441  df-nzr 20529

This theorem is referenced by:  opprnzr  20536  nzrunit  20538  domnring  20567  domnchr  20736  uvcf1  20999  lindfind2  21025  frlmisfrlm  21055  nminvr  23833  deg1pw  25285  ply1nz  25286  ply1remlem  25327  ply1rem  25328  facth1  25329  fta1glem1  25330  fta1glem2  25331  prmidl0  31626  krull  31643  zrhnm  31919  isdomn4  40172  uvcn0  40265  0prjspnlem  40460  mon1pid  41030  mon1psubm  41031  nzrneg1ne0  45427  islindeps2  45824