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  4374  csbprc  4407  ralf0  4514  ralnralall  4519  tgcgr4  28398  frgrregord013  30268  nalfal  35974  imsym1  35989  consym1  35991  dissym1  35992  unisym1  35994  exisym1  35995  subsym1  35998  bj-falor2  36149  bj-prmoore  36681  wl-2mintru2  37057  orfa1  37645  orfa2  37646  bifald  37647  botel  37664  lindslinindsimp2  47659

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »