This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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} (R)$
	Assertion	opprnzr	$⊢ R \in NzRing \to O \in NzRing$

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