Theorem truimtru 1566

Description: A → identity. (Contributed by Anthony Hart, 22-Oct-2010.) An alternate proof is possible using trud 1553 instead of id 22 but the principle of identity id 22 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 22	. 2 ⊢ (⊤ → ⊤)
2	1	bitru 1552	1 ⊢ ((⊤ → ⊤) ↔ ⊤)

Syntax hints:   → wi 4   ↔ wb 209  ⊤wtru 1544

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 210  df-tru 1546

This theorem is referenced by: (None)