Metamath Proof Explorer

Theorem trunortruOLD

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

		Ref	Expression
	Assertion	trunortruOLD	$⊢ (⊤ ⊽ ⊤) \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 ⊥$