Theorem falim 1586

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 1579. (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 1583	. 2 ⊢ ¬ ⊥
2	1	pm2.21i 120	1 ⊢ (⊥ → 𝜑)

This proof depends on syntax axioms:   → wi 4  ⊥wfal 1581

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-tru 1572  df-fal 1582

This theorem is used by:  falimd  1587  tbw-bijust  1730  tbw-negdf  1731  tbw-ax4  1735  merco1  1745  merco2  1768  sbcfal  3812  csbprc  4366  ralnralall  4468  tgcgr4  29003  frgrregord013  31005  nalfal  37287  imsym1  37302  consym1  37304  dissym1  37305  unisym1  37307  exisym1  37308  subsym1  37311  bj-falor2  37551  bj-cbvaw  37636  bj-cbveaw  37638  bj-prmoore  38144  wl-2mintru2  38523  orfa1  39128  orfa2  39129  bifald  39130  botel  39145  quadfac  43364  quantgodelALT  47993  lindslinindsimp2  49683