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