MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  falim Unicode version

Theorem falim 1409
Description: The truth value implies anything. Also called the principle of explosion, or "ex falso quodlibet". (Contributed by FL, 20-Mar-2011.) (Proof shortened by Anthony Hart, 1-Aug-2011.)
Assertion
Ref Expression
falim

Proof of Theorem falim
StepHypRef Expression
1 fal 1402 . 2
21pm2.21i 131 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4   wfal 1400
This theorem is referenced by:  falimd  1410  dfnotOLD  1415  falimtru  1429  tbw-bijust  1531  tbw-negdf  1532  tbw-ax4  1536  merco1  1546  merco2  1569  csbprc  3821  frgrareg  25117  frgraregord013  25118  nalf  29868  imsym1  29883  consym1  29885  dissym1  29886  unisym1  29888  exisym1  29889  orfa1  30484  orfa2  30485  bifald  30486  botel  30506  ralnralall  32294  lindslinindsimp2  33064  bj-falor2  34174
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 185  df-tru 1398  df-fal 1401
  Copyright terms: Public domain W3C validator