Metamath Proof Explorer

Theorem xor

Description: Two ways to express exclusive disjunction ( df-xor ). Theorem *5.22 of WhiteheadRussell p. 124. (Contributed by NM, 3-Jan-2005) (Proof shortened by Wolf Lammen, 22-Jan-2013)

		Ref	Expression
	Assertion	xor	$⊢ \neg (φ \leftrightarrow ψ) \leftrightarrow ((φ \land \neg ψ) \lor (ψ \land \neg φ))$

Proof

Step	Hyp	Ref	Expression
1		iman	$⊢ (φ \to ψ) \leftrightarrow \neg (φ \land \neg ψ)$
2		iman	$⊢ (ψ \to φ) \leftrightarrow \neg (ψ \land \neg φ)$
3	1 2	anbi12i	$⊢ ((φ \to ψ) \land (ψ \to φ)) \leftrightarrow (\neg (φ \land \neg ψ) \land \neg (ψ \land \neg φ))$
4		dfbi2	$⊢ (φ \leftrightarrow ψ) \leftrightarrow ((φ \to ψ) \land (ψ \to φ))$
5		ioran	$⊢ \neg ((φ \land \neg ψ) \lor (ψ \land \neg φ)) \leftrightarrow (\neg (φ \land \neg ψ) \land \neg (ψ \land \neg φ))$
6	3 4 5	3bitr4ri	$⊢ \neg ((φ \land \neg ψ) \lor (ψ \land \neg φ)) \leftrightarrow (φ \leftrightarrow ψ)$
7	6	con1bii	$⊢ \neg (φ \leftrightarrow ψ) \leftrightarrow ((φ \land \neg ψ) \lor (ψ \land \neg φ))$