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

Metamath Proof Explorer

Theorem xor3

Description: Two ways to express "exclusive or". (Contributed by NM, 1-Jan-2006)

Ref Expression
Assertion xor3 ⊢ ¬ φ ↔ ψ ↔ φ ↔ ¬ ψ

Proof

Step Hyp Ref Expression
1 pm5.18 ⊢ φ ↔ ψ ↔ ¬ φ ↔ ¬ ψ
2 1 con2bii ⊢ φ ↔ ¬ ψ ↔ ¬ φ ↔ ψ
3 2 bicomi ⊢ ¬ φ ↔ ψ ↔ φ ↔ ¬ ψ