This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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

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