Theorem falim 1556

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

Syntax hints:   → wi 4  ⊥wfal 1551

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 206  df-tru 1542  df-fal 1552

This theorem is referenced by:  falimd  1557  tbw-bijust  1702  tbw-negdf  1703  tbw-ax4  1707  merco1  1717  merco2  1740  ab0w  4304  csbprc  4337  ralf0  4441  ralnralall  4446  tgcgr4  26796  frgrregord013  28660  nalfal  34519  imsym1  34534  consym1  34536  dissym1  34537  unisym1  34539  exisym1  34540  bj-falor2  34694  bj-prmoore  35213  wl-2mintru2  35589  orfa1  36170  orfa2  36171  bifald  36172  botel  36189  lindslinindsimp2  45692