Metamath Proof Explorer

Theorem truxortru

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

Ref Expression
Assertion truxortru ⊢ ⊤ ⊻ ⊤ ↔ ⊥

Proof

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