Theorem nzrring 19082

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 2610	. . 3 ⊢ (1r‘𝑅) = (1r‘𝑅)
2		eqid 2610	. . 3 ⊢ (0g‘𝑅) = (0g‘𝑅)
3	1, 2	isnzr 19080	. 2 ⊢ (𝑅 ∈ NzRing ↔ (𝑅 ∈ Ring ∧ (1r‘𝑅) ≠ (0g‘𝑅)))
4	3	simplbi 475	1 ⊢ (𝑅 ∈ NzRing → 𝑅 ∈ Ring)

Syntax hints:   → wi 4   ∈ wcel 1977   ≠ wne 2780  ‘cfv 5804  0_gc0g 15923  1_rcur 18324  Ringcrg 18370  NzRingcnzr 19078

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-iota 5768  df-fv 5812  df-nzr 19079

This theorem is referenced by:  opprnzr  19086  nzrunit  19088  domnring  19117  domnchr  19699  uvcf1  19950  lindfind2  19976  frlmisfrlm  20006  nminvr  22283  deg1pw  23684  ply1nz  23685  ply1remlem  23726  ply1rem  23727  facth1  23728  fta1glem1  23729  fta1glem2  23730  zrhnm  29341  mon1pid  36802  mon1psubm  36803  nzrneg1ne0  41659  islindeps2  42066