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

Theorem falim 1557
Description: The truth value implies anything. Also called the "principle of explosion", or "ex falso [sequitur]] quodlibet" (Latin for "from falsehood, anything [follows]]"). Dual statement of trud 1550. (Contributed by FL, 20-Mar-2011.) (Proof shortened by Anthony Hart, 1-Aug-2011.)
Assertion
Ref Expression
falim (⊥ → 𝜑)

Proof of Theorem falim
StepHypRef Expression
1 fal 1554 . 2 ¬ ⊥
21pm2.21i 119 1 (⊥ → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wfal 1552
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 207  df-tru 1543  df-fal 1553
This theorem is referenced by:  falimd  1558  tbw-bijust  1698  tbw-negdf  1699  tbw-ax4  1703  merco1  1713  merco2  1736  ab0w  4378  csbprc  4408  ralf0  4513  ralnralall  4514  tgcgr4  28529  frgrregord013  30404  nalfal  36382  imsym1  36397  consym1  36399  dissym1  36400  unisym1  36402  exisym1  36403  subsym1  36406  bj-falor2  36564  bj-prmoore  37094  wl-2mintru2  37470  orfa1  38070  orfa2  38071  bifald  38072  botel  38089  lindslinindsimp2  48353
  Copyright terms: Public domain W3C validator