dfxor4

Description: Express exclusive-or in terms of implication and negation. Statement in Frege1879 p. 12. (Contributed by RP, 14-Apr-2020)

		Ref	Expression
	Assertion	dfxor4	$⊢ (φ ⊻ ψ) \leftrightarrow \neg ((\neg φ \to ψ) \to \neg (φ \to \neg ψ))$

Step	Hyp	Ref	Expression
1		xor2	$⊢ (φ ⊻ ψ) \leftrightarrow ((φ \lor ψ) \land \neg (φ \land ψ))$
2		df-or	$⊢ (φ \lor ψ) \leftrightarrow (\neg φ \to ψ)$
3		imnan	$⊢ (φ \to \neg ψ) \leftrightarrow \neg (φ \land ψ)$
4	3	bicomi	$⊢ \neg (φ \land ψ) \leftrightarrow (φ \to \neg ψ)$
5	2 4	anbi12i	$⊢ ((φ \lor ψ) \land \neg (φ \land ψ)) \leftrightarrow ((\neg φ \to ψ) \land (φ \to \neg ψ))$
6		df-an	$⊢ ((\neg φ \to ψ) \land (φ \to \neg ψ)) \leftrightarrow \neg ((\neg φ \to ψ) \to \neg (φ \to \neg ψ))$
7	1 5 6	3bitri	$⊢ (φ ⊻ ψ) \leftrightarrow \neg ((\neg φ \to ψ) \to \neg (φ \to \neg ψ))$

Metamath Proof Explorer