Theorem nzrring 20604

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

Syntax hints:   → wi 4   ∈ wcel 2105   ≠ wne 2941  ‘cfv 6465  0_gc0g 17220  1_rcur 19805  Ringcrg 19851  NzRingcnzr 20600

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2708

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2715  df-cleq 2729  df-clel 2815  df-ne 2942  df-rab 3405  df-v 3443  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4268  df-if 4472  df-sn 4572  df-pr 4574  df-op 4578  df-uni 4851  df-br 5088  df-iota 6417  df-fv 6473  df-nzr 20601

This theorem is referenced by:  opprnzr  20608  nzrunit  20610  domnring  20639  domnchr  20808  uvcf1  21071  lindfind2  21097  frlmisfrlm  21127  nminvr  23905  deg1pw  25357  ply1nz  25358  ply1remlem  25399  ply1rem  25400  facth1  25401  fta1glem1  25402  fta1glem2  25403  prmidl0  31731  krull  31748  zrhnm  32025  isdomn4  40380  uvcn0  40468  0prjspnlem  40663  mon1pid  41234  mon1psubm  41235  nzrneg1ne0  45679  islindeps2  46076