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	$⊢ (⊥ ⊻ ⊤) \leftrightarrow ⊤$

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