Theorem opprnzr

Description: The opposite of a nonzero ring is nonzero. (Contributed by Mario Carneiro, 17-Jun-2015)

	Ref	Expression
Hypothesis	opprnzr.1	$$⊢O={opp}_r\left(R\right)$$
Assertion	opprnzr	$$⊢R\in \mathrm{NzRing}\to O\in \mathrm{NzRing}$$

Proof

Step	Hyp	Ref	Expression
1		opprnzr.1	$$⊢O={opp}_r\left(R\right)$$
2	1	opprnzrb	$$⊢R\in \mathrm{NzRing}\leftrightarrow O\in \mathrm{NzRing}$$
3	2	biimpi	$$⊢R\in \mathrm{NzRing}\to O\in \mathrm{NzRing}$$