Metamath Proof Explorer

Theorem truxorfal

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

Ref Expression
Assertion truxorfal ⊢ ⊤ ⊻ ⊥ ↔ ⊤

Proof

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