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 ⊢⊤⊻⊥↔⊤