Theorem nbn2

Description: The negation of a wff is equivalent to the wff's equivalence to falsehood. (Contributed by Juha Arpiainen, 19-Jan-2006) (Proof shortened by Wolf Lammen, 28-Jan-2013)

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

Proof

Step	Hyp	Ref	Expression
1		pm5.501	$$⊢\neg \phi \to \left(\neg \psi \leftrightarrow \left(\neg \phi \leftrightarrow \neg \psi \right)\right)$$
2		notbi	$$⊢\left(\phi \leftrightarrow \psi \right)\leftrightarrow \left(\neg \phi \leftrightarrow \neg \psi \right)$$
3	1 2	bitr4di	$$⊢\neg \phi \to \left(\neg \psi \leftrightarrow \left(\phi \leftrightarrow \psi \right)\right)$$