Theorem truimtru 1592

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

Assertion

Ref	Expression
truimtru	⊢ ((⊤ → ⊤) ↔ ⊤)

Proof of Theorem truimtru

Step	Hyp	Ref	Expression
1		id 23	. 2 ⊢ (⊤ → ⊤)
2	1	bitru 1578	1 ⊢ ((⊤ → ⊤) ↔ ⊤)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  ⊤wtru 1570

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-tru 1572

This theorem is used by: (None)