Theorem nzrring 20034

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

Syntax hints:   → wi 4   ∈ wcel 2114   ≠ wne 3016  ‘cfv 6355  0_gc0g 16713  1_rcur 19251  Ringcrg 19297  NzRingcnzr 20030

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 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-iota 6314  df-fv 6363  df-nzr 20031

This theorem is referenced by:  opprnzr  20038  nzrunit  20040  domnring  20069  domnchr  20679  uvcf1  20936  lindfind2  20962  frlmisfrlm  20992  nminvr  23278  deg1pw  24714  ply1nz  24715  ply1remlem  24756  ply1rem  24757  facth1  24758  fta1glem1  24759  fta1glem2  24760  krull  30980  zrhnm  31210  uvcn0  39171  0prjspnlem  39288  mon1pid  39825  mon1psubm  39826  nzrneg1ne0  44160  islindeps2  44558