Metamath Proof Explorer

Theorem trunortru

Description: A -\/ identity. (Contributed by Remi, 25-Oct-2023) (Proof shortened by Wolf Lammen, 7-Dec-2023)

		Ref	Expression
	Assertion	trunortru	$⊢ (⊤ ⊽ ⊤) \leftrightarrow ⊥$

Step	Hyp	Ref	Expression
1		df-nor	$⊢ (⊤ ⊽ ⊤) \leftrightarrow \neg (⊤ \lor ⊤)$
2		truortru	$⊢ (⊤ \lor ⊤) \leftrightarrow ⊤$
3	1 2	xchbinx	$⊢ (⊤ ⊽ ⊤) \leftrightarrow \neg ⊤$
4		df-fal	$⊢ ⊥ \leftrightarrow \neg ⊤$
5	3 4	bitr4i	$⊢ (⊤ ⊽ ⊤) \leftrightarrow ⊥$