Theorem falim 1552

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

Syntax hints:   → wi 4  ⊥wfal 1547

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 1538  df-fal 1548

This theorem is referenced by:  falimd  1553  tbw-bijust  1693  tbw-negdf  1694  tbw-ax4  1698  merco1  1708  merco2  1731  ab0w  4385  csbprc  4415  ralf0  4520  ralnralall  4521  tgcgr4  28536  frgrregord013  30406  nalfal  36346  imsym1  36361  consym1  36363  dissym1  36364  unisym1  36366  exisym1  36367  subsym1  36370  bj-falor2  36528  bj-prmoore  37058  wl-2mintru2  37434  orfa1  38032  orfa2  38033  bifald  38034  botel  38051  lindslinindsimp2  48237