MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  truimtru Structured version   Visualization version   GIF version

Theorem truimtru 1530
Description: A identity. (Contributed by Anthony Hart, 22-Oct-2010.) An alternate proof is possible using trud 1517 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
StepHypRef Expression
1 id 22 . 2 (⊤ → ⊤)
21bitru 1516 1 ((⊤ → ⊤) ↔ ⊤)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wtru 1508
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 199  df-tru 1510
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator