Theorem falim 1587

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

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

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 1573  df-fal 1583

This theorem is used by:  falimd  1588  tbw-bijust  1731  tbw-negdf  1732  tbw-ax4  1736  merco1  1746  merco2  1769  sbcfal  3816  csbprc  4370  ralnralall  4472  tgcgr4  29051  frgrregord013  31053  nalfal  37406  imsym1  37421  consym1  37423  dissym1  37424  unisym1  37426  exisym1  37427  subsym1  37430  bj-falor2  37670  bj-cbvaw  37755  bj-cbveaw  37757  bj-prmoore  38306  wl-2mintru2  38682  orfa1  39285  orfa2  39286  bifald  39287  botel  39302  quadfac  43521  quantgodelALT  48158  lindslinindsimp2  49906