Metamath Proof Explorer

Theorem falimfal

Description: A -> identity. (Contributed by Anthony Hart, 22-Oct-2010) An alternate proof is possible using falim instead of id but the present proof using id emphasizes that the result does not require the principle of explosion. (Proof modification is discouraged.)

		Ref	Expression
	Assertion	falimfal	$⊢ (⊥ \to ⊥) \leftrightarrow ⊤$

Proof

Step	Hyp	Ref	Expression
1		id	$⊢ ⊥ \to ⊥$
2	1	bitru	$⊢ (⊥ \to ⊥) \leftrightarrow ⊤$