Theorem domnring 20675

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

Syntax hints:   → wi 4   ∈ wcel 2114  Ringcrg 20205  NzRingcnzr 20480  Domncdomn 20660

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-nul 5241

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rab 3391  df-v 3432  df-sbc 3730  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-iota 6448  df-fv 6500  df-ov 7363  df-nzr 20481  df-domn 20663

This theorem is referenced by:  domneq0  20676  isdomn4  20684  domneq0r  20692  fidomndrnglem  20740  fidomndrng  20741  abvtrivg  20801  domnchr  21522  znidomb  21551  deg1ldgdomn  26069  deg1mul  26090  ply1domn  26099  r1pid2  26137  domnprodn0  33351  deg1prod  33658  r1peuqusdeg1  35841  deg1pow  42594  domnexpgn0cl  42982  fidomncyc  42994  proot1mul  43640  proot1hash  43641  deg1mhm  43646  lidldomn1  48719  uzlidlring  48723  domnmsuppn0  48857