Metamath Proof Explorer

Theorem falxorfal

Description: A \/_ identity. (Contributed by David A. Wheeler, 9-May-2015)

Ref Expression
Assertion falxorfal ⊢ ⊥ ⊻ ⊥ ↔ ⊥

Proof

Step Hyp Ref Expression
1 df-xor ⊢ ⊥ ⊻ ⊥ ↔ ¬ ⊥ ↔ ⊥
2 falbifal ⊢ ⊥ ↔ ⊥ ↔ ⊤
3 1 2 xchbinx ⊢ ⊥ ⊻ ⊥ ↔ ¬ ⊤
4 nottru ⊢ ¬ ⊤ ↔ ⊥
5 3 4 bitri ⊢ ⊥ ⊻ ⊥ ↔ ⊥