Metamath Proof Explorer

Theorem truimtru

Description: A -> identity. (Contributed by Anthony Hart, 22-Oct-2010) An alternate proof is possible using trud instead of id but the principle of identity id is more basic, and the present proof indicates that the result still holds in relevance logic. (Proof modification is discouraged.)

		Ref	Expression
	Assertion	truimtru	$⊢ (⊤ \to ⊤) \leftrightarrow ⊤$

Proof

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