Theorem domnring 20729

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

Syntax hints:   → wi 4   ∈ wcel 2108  Ringcrg 20260  NzRingcnzr 20538  Domncdomn 20714

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-nul 5324

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ne 2947  df-ral 3068  df-rab 3444  df-v 3490  df-sbc 3805  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-iota 6525  df-fv 6581  df-ov 7451  df-nzr 20539  df-domn 20717

This theorem is referenced by:  domneq0  20730  isdomn4  20738  domneq0r  20746  fidomndrnglem  20795  fidomndrng  20796  abvtrivg  20856  domnchr  21570  znidomb  21603  deg1ldgdomn  26153  deg1mul  26174  ply1domn  26183  r1pid2  26221  domnprodn0  33247  r1peuqusdeg1  35611  deg1pow  42098  domnexpgn0cl  42478  fidomncyc  42490  proot1mul  43155  proot1hash  43156  deg1mhm  43161  lidldomn1  47954  uzlidlring  47958  domnmsuppn0  48094