Metamath Proof Explorer

Theorem trunorfal

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

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

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