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

This theorem is referenced by:  falimd  1559  tbw-bijust  1700  tbw-negdf  1701  tbw-ax4  1705  merco1  1715  merco2  1738  ab0w  4372  csbprc  4405  ralf0  4512  ralnralall  4517  tgcgr4  27771  frgrregord013  29637  nalfal  35276  imsym1  35291  consym1  35293  dissym1  35294  unisym1  35296  exisym1  35297  subsym1  35300  bj-falor2  35451  bj-prmoore  35984  wl-2mintru2  36360  orfa1  36941  orfa2  36942  bifald  36943  botel  36960  lindslinindsimp2  47097