Metamath Proof Explorer

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 ⊢ φ ⊻ ψ ↔ φ ∧ ¬ ψ ∨ ¬ φ ∧ ψ