Theorem falim 1577

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

Syntax hints:   → wi 4  ⊥wfal 1572

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 209  df-tru 1563  df-fal 1573

This theorem is referenced by:  falimd  1578  tbw-bijust  1718  tbw-negdf  1719  tbw-ax4  1723  merco1  1733  merco2  1756  csbprc  4363  ralnralall  4467  tgcgr4  28697  frgrregord013  30594  nalfal  36760  imsym1  36775  consym1  36777  dissym1  36778  unisym1  36780  exisym1  36781  subsym1  36784  bj-falor2  37025  bj-cbvaw  37110  bj-cbveaw  37112  bj-prmoore  37602  wl-2mintru2  37982  orfa1  38581  orfa2  38582  bifald  38583  botel  38600  quantgodelALT  47446  lindslinindsimp2  49082