Metamath Proof Explorer

Theorem falnorfal

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

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

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