Theorem domnring 20835

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 20834	. 2 ⊢ (𝑅 ∈ Domn → 𝑅 ∈ NzRing)
2		nzrring 20642	. 2 ⊢ (𝑅 ∈ NzRing → 𝑅 ∈ Ring)
3	1, 2	syl 18	1 ⊢ (𝑅 ∈ Domn → 𝑅 ∈ Ring)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  Ringcrg 20338  NzRingcnzr 20638  Domncdomn 20820

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737  ax-nul 5271

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-ral 3082  df-rab 3419  df-v 3459  df-sbc 3747  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-iota 6496  df-fv 6548  df-ov 7419  df-nzr 20639  df-domn 20823

This theorem is used by:  domneq0  20836  isdomn4  20843  domneq0r  20851  fidomndrnglem  20905  fidomndrng  20906  abvtrivg  20965  domnchr  21711  znidomb  21740  deg1ldgdomn  26280  deg1mul  26301  ply1domn  26310  r1pid2  26348  domnprodn0  33621  deg1prod  33896  r1peuqusdeg1  36148  deg1pow  42941  domnexpgn0cl  43324  fidomncyc  43336  proot1mul  43954  proot1hash  43955  deg1mhm  43960  lidldomn1  49029  uzlidlring  49033  domnmsuppn0  49182