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  1701  tbw-negdf  1702  tbw-ax4  1706  merco1  1716  merco2  1739  ab0w  4307  csbprc  4340  ralf0  4444  ralnralall  4449  tgcgr4  26892  frgrregord013  28759  nalfal  34592  imsym1  34607  consym1  34609  dissym1  34610  unisym1  34612  exisym1  34613  bj-falor2  34767  bj-prmoore  35286  wl-2mintru2  35662  orfa1  36243  orfa2  36244  bifald  36245  botel  36262  lindslinindsimp2  45804