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  4338  csbprc  4368  ralf0  4473  ralnralall  4474  tgcgr4  28434  frgrregord013  30297  nalfal  36364  imsym1  36379  consym1  36381  dissym1  36382  unisym1  36384  exisym1  36385  subsym1  36388  bj-falor2  36546  bj-prmoore  37076  wl-2mintru2  37452  orfa1  38052  orfa2  38053  bifald  38054  botel  38071  lindslinindsimp2  48425