Metamath Proof Explorer

Theorem trunorfalOLD

Description: Obsolete version of trunorfal as of 17-Dec-2023. (Contributed by Remi, 25-Oct-2023) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		df-nor	$⊢ (⊤ ⊽ ⊥) \leftrightarrow \neg (⊤ \lor ⊥)$
2		tru	$⊢ ⊤$
3	2	orci	$⊢ (⊤ \lor ⊥)$
4	3	notnoti	$⊢ \neg \neg (⊤ \lor ⊥)$
5	4	bifal	$⊢ \neg (⊤ \lor ⊥) \leftrightarrow ⊥$
6	1 5	bitri	$⊢ (⊤ ⊽ ⊥) \leftrightarrow ⊥$