Theorem falim 1556

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

Syntax hints:   → wi 4  ⊥wfal 1551

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 1542  df-fal 1552

This theorem is referenced by:  falimd  1557  tbw-bijust  1697  tbw-negdf  1698  tbw-ax4  1702  merco1  1712  merco2  1735  ab0w  4359  csbprc  4389  ralf0  4494  ralnralall  4495  tgcgr4  28476  frgrregord013  30343  nalfal  36379  imsym1  36394  consym1  36396  dissym1  36397  unisym1  36399  exisym1  36400  subsym1  36403  bj-falor2  36561  bj-prmoore  37091  wl-2mintru2  37467  orfa1  38067  orfa2  38068  bifald  38069  botel  38086  lindslinindsimp2  48353