Theorem neor

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

	Ref	Expression
Assertion	neor	|- ( ( A = B \/ ps ) <-> ( A =/= B -> ps ) )

Proof

Step	Hyp	Ref	Expression
1		df-or	|- ( ( A = B \/ ps ) <-> ( -. A = B -> ps ) )
2		df-ne	|- ( A =/= B <-> -. A = B )
3	2	imbi1i	|- ( ( A =/= B -> ps ) <-> ( -. A = B -> ps ) )
4	1 3	bitr4i	|- ( ( A = B \/ ps ) <-> ( A =/= B -> ps ) )