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

Metamath Proof Explorer

Theorem neor

Description: Logical OR with an equality. (Contributed by NM, 29-Apr-2007)

		Ref	Expression
	Assertion	neor	$⊢ (A = B \lor ψ) \leftrightarrow (A \neq B \to ψ)$

Step	Hyp	Ref	Expression
1		df-or	$⊢ (A = B \lor ψ) \leftrightarrow (\neg A = B \to ψ)$
2		df-ne	$⊢ A \neq B \leftrightarrow \neg A = B$
3	2	imbi1i	$⊢ (A \neq B \to ψ) \leftrightarrow (\neg A = B \to ψ)$
4	1 3	bitr4i	$⊢ (A = B \lor ψ) \leftrightarrow (A \neq B \to ψ)$