Theorem pm5.18

Description: Theorem *5.18 of WhiteheadRussell p. 124. This theorem says that logical equivalence is the same as negated "exclusive or". (Contributed by NM, 28-Jun-2002) (Proof shortened by Andrew Salmon, 20-Jun-2011) (Proof shortened by Wolf Lammen, 15-Oct-2013)

	Ref	Expression
Assertion	pm5.18	$$⊢\left(\phi \leftrightarrow \psi \right)\leftrightarrow \neg \left(\phi \leftrightarrow \neg \psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		pm5.501	$$⊢\phi \to \left(\neg \psi \leftrightarrow \left(\phi \leftrightarrow \neg \psi \right)\right)$$
2	1	con1bid	$$⊢\phi \to \left(\neg \left(\phi \leftrightarrow \neg \psi \right)\leftrightarrow \psi \right)$$
3		pm5.501	$$⊢\phi \to \left(\psi \leftrightarrow \left(\phi \leftrightarrow \psi \right)\right)$$
4	2 3	bitr2d	$$⊢\phi \to \left(\left(\phi \leftrightarrow \psi \right)\leftrightarrow \neg \left(\phi \leftrightarrow \neg \psi \right)\right)$$
5		nbn2	$$⊢\neg \phi \to \left(\neg \neg \psi \leftrightarrow \left(\phi \leftrightarrow \neg \psi \right)\right)$$
6	5	con1bid	$$⊢\neg \phi \to \left(\neg \left(\phi \leftrightarrow \neg \psi \right)\leftrightarrow \neg \psi \right)$$
7		nbn2	$$⊢\neg \phi \to \left(\neg \psi \leftrightarrow \left(\phi \leftrightarrow \psi \right)\right)$$
8	6 7	bitr2d	$$⊢\neg \phi \to \left(\left(\phi \leftrightarrow \psi \right)\leftrightarrow \neg \left(\phi \leftrightarrow \neg \psi \right)\right)$$
9	4 8	pm2.61i	$$⊢\left(\phi \leftrightarrow \psi \right)\leftrightarrow \neg \left(\phi \leftrightarrow \neg \psi \right)$$