Theorem falim 1559

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

Syntax hints:   → wi 4  ⊥wfal 1554

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 1545  df-fal 1555

This theorem is referenced by:  falimd  1560  tbw-bijust  1701  tbw-negdf  1702  tbw-ax4  1706  merco1  1716  merco2  1739  ab0w  4374  csbprc  4407  ralf0  4514  ralnralall  4519  tgcgr4  27782  frgrregord013  29648  nalfal  35288  imsym1  35303  consym1  35305  dissym1  35306  unisym1  35308  exisym1  35309  subsym1  35312  bj-falor2  35463  bj-prmoore  35996  wl-2mintru2  36372  orfa1  36953  orfa2  36954  bifald  36955  botel  36972  lindslinindsimp2  47144