Theorem falim 1558

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 1551. (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 1555	. 2 ⊢ ¬ ⊥
2	1	pm2.21i 119	1 ⊢ (⊥ → 𝜑)

Syntax hints:   → wi 4  ⊥wfal 1553

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 1544  df-fal 1554

This theorem is referenced by:  falimd  1559  tbw-bijust  1699  tbw-negdf  1700  tbw-ax4  1704  merco1  1714  merco2  1737  ab0w  4324  csbprc  4354  ralf0  4459  ralnralall  4460  tgcgr4  28504  frgrregord013  30367  nalfal  36437  imsym1  36452  consym1  36454  dissym1  36455  unisym1  36457  exisym1  36458  subsym1  36461  bj-falor2  36619  bj-prmoore  37149  wl-2mintru2  37525  orfa1  38125  orfa2  38126  bifald  38127  botel  38144  lindslinindsimp2  48495