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	⊢ ( ¬ ( 𝜑 ↔ 𝜓 ) → ( 𝜑 ∨ 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		norbi	⊢ ( ¬ ( 𝜑 ∨ 𝜓 ) → ( 𝜑 ↔ 𝜓 ) )
2	1	con1i	⊢ ( ¬ ( 𝜑 ↔ 𝜓 ) → ( 𝜑 ∨ 𝜓 ) )