Theorem domnring 20611

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

Syntax hints:   → wi 4   ∈ wcel 2109  Ringcrg 20137  NzRingcnzr 20416  Domncdomn 20596

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-nul 5248

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rab 3397  df-v 3440  df-sbc 3745  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-iota 6442  df-fv 6494  df-ov 7356  df-nzr 20417  df-domn 20599

This theorem is referenced by:  domneq0  20612  isdomn4  20620  domneq0r  20628  fidomndrnglem  20676  fidomndrng  20677  abvtrivg  20737  domnchr  21458  znidomb  21487  deg1ldgdomn  26016  deg1mul  26037  ply1domn  26046  r1pid2  26084  domnprodn0  33234  r1peuqusdeg1  35635  deg1pow  42134  domnexpgn0cl  42516  fidomncyc  42528  proot1mul  43187  proot1hash  43188  deg1mhm  43193  lidldomn1  48235  uzlidlring  48239  domnmsuppn0  48373