Theorem falxortru

Description: A \/_ identity. (Contributed by David A. Wheeler, 9-May-2015) (Proof shortened by Wolf Lammen, 10-Jul-2020)

	Ref	Expression
Assertion	falxortru	⊢ ( ( ⊥ ⊻ ⊤ ) ↔ ⊤ )

Proof

Step	Hyp	Ref	Expression
1		xorcom	⊢ ( ( ⊥ ⊻ ⊤ ) ↔ ( ⊤ ⊻ ⊥ ) )
2		truxorfal	⊢ ( ( ⊤ ⊻ ⊥ ) ↔ ⊤ )
3	1 2	bitri	⊢ ( ( ⊥ ⊻ ⊤ ) ↔ ⊤ )