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	$⊢ ((φ \lor ψ) \land \neg (φ \land ψ)) \leftrightarrow (φ \leftrightarrow \neg ψ)$

Step	Hyp	Ref	Expression
1		bicom	$⊢ (φ \leftrightarrow \neg ψ) \leftrightarrow (\neg ψ \leftrightarrow φ)$
2		dfbi2	$⊢ (\neg ψ \leftrightarrow φ) \leftrightarrow ((\neg ψ \to φ) \land (φ \to \neg ψ))$
3		orcom	$⊢ (φ \lor ψ) \leftrightarrow (ψ \lor φ)$
4		df-or	$⊢ (ψ \lor φ) \leftrightarrow (\neg ψ \to φ)$
5	3 4	bitr2i	$⊢ (\neg ψ \to φ) \leftrightarrow (φ \lor ψ)$
6		imnan	$⊢ (φ \to \neg ψ) \leftrightarrow \neg (φ \land ψ)$
7	5 6	anbi12i	$⊢ ((\neg ψ \to φ) \land (φ \to \neg ψ)) \leftrightarrow ((φ \lor ψ) \land \neg (φ \land ψ))$
8	1 2 7	3bitrri	$⊢ ((φ \lor ψ) \land \neg (φ \land ψ)) \leftrightarrow (φ \leftrightarrow \neg ψ)$

Metamath Proof Explorer