Theorem bibif

Description: Transfer negation via an equivalence. (Contributed by NM, 3-Oct-2007) (Proof shortened by Wolf Lammen, 28-Jan-2013)

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

Proof

Step	Hyp	Ref	Expression
1		nbn2	$$⊢\neg \psi \to \left(\neg \phi \leftrightarrow \left(\psi \leftrightarrow \phi \right)\right)$$
2		bicom	$$⊢\left(\psi \leftrightarrow \phi \right)\leftrightarrow \left(\phi \leftrightarrow \psi \right)$$
3	1 2	bitr2di	$$⊢\neg \psi \to \left(\left(\phi \leftrightarrow \psi \right)\leftrightarrow \neg \phi \right)$$