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

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

Proof of Theorem falimfal
StepHypRef Expression
1 id 22 . 2 (⊥ → ⊥)
21bitru 1552 1 ((⊥ → ⊥) ↔ ⊤)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wtru 1544  wfal 1555
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)
  Copyright terms: Public domain W3C validator