Theorem falim 1554

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

Syntax hints:   → wi 4  ⊥wfal 1549

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 207  df-tru 1540  df-fal 1550

This theorem is referenced by:  falimd  1555  tbw-bijust  1696  tbw-negdf  1697  tbw-ax4  1701  merco1  1711  merco2  1734  ab0w  4401  csbprc  4432  ralf0  4537  ralnralall  4538  tgcgr4  28549  frgrregord013  30419  nalfal  36361  imsym1  36376  consym1  36378  dissym1  36379  unisym1  36381  exisym1  36382  subsym1  36385  bj-falor2  36543  bj-prmoore  37073  wl-2mintru2  37449  orfa1  38037  orfa2  38038  bifald  38039  botel  38056  lindslinindsimp2  48181