Theorem excxor

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

	Ref	Expression
Assertion	excxor	⊢ ( ( 𝜑 ⊻ 𝜓 ) ↔ ( ( 𝜑 ∧ ¬ 𝜓 ) ∨ ( ¬ 𝜑 ∧ 𝜓 ) ) )

Proof

Step	Hyp	Ref	Expression
1		df-xor	⊢ ( ( 𝜑 ⊻ 𝜓 ) ↔ ¬ ( 𝜑 ↔ 𝜓 ) )
2		xor	⊢ ( ¬ ( 𝜑 ↔ 𝜓 ) ↔ ( ( 𝜑 ∧ ¬ 𝜓 ) ∨ ( 𝜓 ∧ ¬ 𝜑 ) ) )
3		ancom	⊢ ( ( 𝜓 ∧ ¬ 𝜑 ) ↔ ( ¬ 𝜑 ∧ 𝜓 ) )
4	3	orbi2i	⊢ ( ( ( 𝜑 ∧ ¬ 𝜓 ) ∨ ( 𝜓 ∧ ¬ 𝜑 ) ) ↔ ( ( 𝜑 ∧ ¬ 𝜓 ) ∨ ( ¬ 𝜑 ∧ 𝜓 ) ) )
5	1 2 4	3bitri	⊢ ( ( 𝜑 ⊻ 𝜓 ) ↔ ( ( 𝜑 ∧ ¬ 𝜓 ) ∨ ( ¬ 𝜑 ∧ 𝜓 ) ) )