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

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

Syntax hints:   → wi 4   ∈ wcel 2144   ≠ wne 2942  ‘cfv 6031  0_gc0g 16307  1_rcur 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