This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem falimtru

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

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

Proof

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