This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem excxor

Description: This tautology shows that xor is really exclusive. (Contributed by FL, 22-Nov-2010)

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

Step	Hyp	Ref	Expression
1		df-xor	$⊢ (φ ⊻ ψ) \leftrightarrow \neg (φ \leftrightarrow ψ)$
2		xor	$⊢ \neg (φ \leftrightarrow ψ) \leftrightarrow ((φ \land \neg ψ) \lor (ψ \land \neg φ))$
3		ancom	$⊢ (ψ \land \neg φ) \leftrightarrow (\neg φ \land ψ)$
4	3	orbi2i	$⊢ ((φ \land \neg ψ) \lor (ψ \land \neg φ)) \leftrightarrow ((φ \land \neg ψ) \lor (\neg φ \land ψ))$
5	1 2 4	3bitri	$⊢ (φ ⊻ ψ) \leftrightarrow ((φ \land \neg ψ) \lor (\neg φ \land ψ))$