Theorem pm5.17

Description: Theorem *5.17 of WhiteheadRussell p. 124. (Contributed by NM, 3-Jan-2005) (Proof shortened by Wolf Lammen, 3-Jan-2013)

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

Proof

Step	Hyp	Ref	Expression
1		bicom	$$⊢\left(\phi \leftrightarrow \neg \psi \right)\leftrightarrow \left(\neg \psi \leftrightarrow \phi \right)$$
2		dfbi2	$$⊢\left(\neg \psi \leftrightarrow \phi \right)\leftrightarrow \left(\left(\neg \psi \to \phi \right)\wedge \left(\phi \to \neg \psi \right)\right)$$
3		orcom	$$⊢\left(\phi \vee \psi \right)\leftrightarrow \left(\psi \vee \phi \right)$$
4		df-or	$$⊢\left(\psi \vee \phi \right)\leftrightarrow \left(\neg \psi \to \phi \right)$$
5	3 4	bitr2i	$$⊢\left(\neg \psi \to \phi \right)\leftrightarrow \left(\phi \vee \psi \right)$$
6		imnan	$$⊢\left(\phi \to \neg \psi \right)\leftrightarrow \neg \left(\phi \wedge \psi \right)$$
7	5 6	anbi12i	$$⊢\left(\left(\neg \psi \to \phi \right)\wedge \left(\phi \to \neg \psi \right)\right)\leftrightarrow \left(\left(\phi \vee \psi \right)\wedge \neg \left(\phi \wedge \psi \right)\right)$$
8	1 2 7	3bitrri	$$⊢\left(\left(\phi \vee \psi \right)\wedge \neg \left(\phi \wedge \psi \right)\right)\leftrightarrow \left(\phi \leftrightarrow \neg \psi \right)$$