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

This theorem is referenced by:  falimd  1551  tbw-bijust  1692  tbw-negdf  1693  tbw-ax4  1697  merco1  1707  merco2  1730  ab0w  4375  csbprc  4408  ralf0  4515  ralnralall  4520  tgcgr4  28407  frgrregord013  30277  nalfal  36018  imsym1  36033  consym1  36035  dissym1  36036  unisym1  36038  exisym1  36039  subsym1  36042  bj-falor2  36193  bj-prmoore  36725  wl-2mintru2  37101  orfa1  37689  orfa2  37690  bifald  37691  botel  37708  lindslinindsimp2  47717