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

Theorem falimtru 1559
Description: A identity. (Contributed by Anthony Hart, 22-Oct-2010.) An alternate proof is possible using falim 1551 instead of trud 1544 but the present proof using trud 1544 emphasizes that the result does not require the principle of explosion. (Proof modification is discouraged.)
Assertion
Ref Expression
falimtru ((⊥ → ⊤) ↔ ⊤)

Proof of Theorem falimtru
StepHypRef Expression
1 trud 1544 . 2 (⊥ → ⊤)
21bitru 1543 1 ((⊥ → ⊤) ↔ ⊤)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wtru 1535  wfal 1546
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 206  df-tru 1537
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator