Metamath Proof Explorer

Theorem trunantru

Description: A -/\ identity. (Contributed by Anthony Hart, 22-Oct-2010) (Proof shortened by Andrew Salmon, 13-May-2011)

		Ref	Expression
	Assertion	trunantru	$⊢ (⊤ ⊼ ⊤) \leftrightarrow ⊥$

Step	Hyp	Ref	Expression
1		nannot	$⊢ \neg ⊤ \leftrightarrow (⊤ ⊼ ⊤)$
2		nottru	$⊢ \neg ⊤ \leftrightarrow ⊥$
3	1 2	bitr3i	$⊢ (⊤ ⊼ ⊤) \leftrightarrow ⊥$