Metamath Proof Explorer

Theorem falnanfal

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

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

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