Theorem domnring 20617

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

Syntax hints:   → wi 4   ∈ wcel 2111  Ringcrg 20146  NzRingcnzr 20422  Domncdomn 20602

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 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-nul 5239

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ne 2929  df-ral 3048  df-rab 3396  df-v 3438  df-sbc 3737  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4279  df-if 4471  df-sn 4572  df-pr 4574  df-op 4578  df-uni 4855  df-br 5087  df-iota 6432  df-fv 6484  df-ov 7344  df-nzr 20423  df-domn 20605

This theorem is referenced by:  domneq0  20618  isdomn4  20626  domneq0r  20634  fidomndrnglem  20682  fidomndrng  20683  abvtrivg  20743  domnchr  21464  znidomb  21493  deg1ldgdomn  26021  deg1mul  26042  ply1domn  26051  r1pid2  26089  domnprodn0  33234  r1peuqusdeg1  35679  deg1pow  42174  domnexpgn0cl  42556  fidomncyc  42568  proot1mul  43227  proot1hash  43228  deg1mhm  43233  lidldomn1  48262  uzlidlring  48266  domnmsuppn0  48400