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

Step	Hyp	Ref	Expression
1		fal 1554	. 2 ⊢ ¬ ⊥
2	1	pm2.21i 119	1 ⊢ (⊥ → 𝜑)

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  4342  csbprc  4372  ralf0  4477  ralnralall  4478  tgcgr4  28458  frgrregord013  30324  nalfal  36391  imsym1  36406  consym1  36408  dissym1  36409  unisym1  36411  exisym1  36412  subsym1  36415  bj-falor2  36573  bj-prmoore  37103  wl-2mintru2  37479  orfa1  38079  orfa2  38080  bifald  38081  botel  38098  lindslinindsimp2  48452