Theorem nbior

Description: If two propositions are not equivalent, then at least one is true. (Contributed by BJ, 19-Apr-2019) (Proof shortened by Wolf Lammen, 19-Jan-2020)

	Ref	Expression
Assertion	nbior	$$⊢\neg \left(\phi \leftrightarrow \psi \right)\to \left(\phi \vee \psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		norbi	$$⊢\neg \left(\phi \vee \psi \right)\to \left(\phi \leftrightarrow \psi \right)$$
2	1	con1i	$$⊢\neg \left(\phi \leftrightarrow \psi \right)\to \left(\phi \vee \psi \right)$$