Theorem falim 1550

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

Syntax hints:   → wi 4  ⊥wfal 1545

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 1536  df-fal 1546

This theorem is referenced by:  falimd  1551  tbw-bijust  1695  tbw-negdf  1696  tbw-ax4  1700  merco1  1710  merco2  1733  csbprc  4357  ralnralall  4457  tgcgr4  26311  frgrregord013  28168  nalfal  33746  imsym1  33761  consym1  33763  dissym1  33764  unisym1  33766  exisym1  33767  bj-falor2  33914  bj-prmoore  34401  orfa1  35357  orfa2  35358  bifald  35359  botel  35376  lindslinindsimp2  44512