Theorem domnring 20707

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

Syntax hints:   → wi 4   ∈ wcel 2108  Ringcrg 20230  NzRingcnzr 20512  Domncdomn 20692

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-nul 5306

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-ral 3062  df-rab 3437  df-v 3482  df-sbc 3789  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-iota 6514  df-fv 6569  df-ov 7434  df-nzr 20513  df-domn 20695

This theorem is referenced by:  domneq0  20708  isdomn4  20716  domneq0r  20724  fidomndrnglem  20773  fidomndrng  20774  abvtrivg  20834  domnchr  21547  znidomb  21580  deg1ldgdomn  26133  deg1mul  26154  ply1domn  26163  r1pid2  26201  domnprodn0  33279  r1peuqusdeg1  35648  deg1pow  42142  domnexpgn0cl  42533  fidomncyc  42545  proot1mul  43206  proot1hash  43207  deg1mhm  43212  lidldomn1  48147  uzlidlring  48151  domnmsuppn0  48285