Theorem domnring 20744

Description: A domain is a ring. (Contributed by Mario Carneiro, 28-Mar-2015.)

Assertion

Ref	Expression
domnring	⊢ (𝑅 ∈ Domn → 𝑅 ∈ Ring)

Proof of Theorem domnring

Step	Hyp	Ref	Expression
1		domnnzr 20743	. 2 ⊢ (𝑅 ∈ Domn → 𝑅 ∈ NzRing)
2		nzrring 20553	. 2 ⊢ (𝑅 ∈ NzRing → 𝑅 ∈ Ring)
3	1, 2	syl 17	1 ⊢ (𝑅 ∈ Domn → 𝑅 ∈ Ring)

Syntax hints:   → wi 4   ∈ wcel 2141  Ringcrg 20270  NzRingcnzr 20549  Domncdomn 20729

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-nul 5253

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3076  df-rab 3414  df-v 3455  df-sbc 3743  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-if 4478  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-br 5098  df-iota 6472  df-fv 6524  df-ov 7394  df-nzr 20550  df-domn 20732

This theorem is referenced by:  domneq0  20745  isdomn4  20753  domneq0r  20761  fidomndrnglem  20809  fidomndrng  20810  abvtrivg  20870  domnchr  21572  znidomb  21601  deg1ldgdomn  26142  deg1mul  26163  ply1domn  26172  r1pid2  26210  domnprodn0  33420  deg1prod  33740  r1peuqusdeg1  35954  deg1pow  42719  domnexpgn0cl  43102  fidomncyc  43114  proot1mul  43732  proot1hash  43733  deg1mhm  43738  lidldomn1  48814  uzlidlring  48818  domnmsuppn0  48952