![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > falim | Structured version Visualization version GIF version |
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 1550. (Contributed by FL, 20-Mar-2011.) (Proof shortened by Anthony Hart, 1-Aug-2011.) |
Ref | Expression |
---|---|
falim | ⊢ (⊥ → 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fal 1554 | . 2 ⊢ ¬ ⊥ | |
2 | 1 | pm2.21i 119 | 1 ⊢ (⊥ → 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ⊥wfal 1552 |
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 1543 df-fal 1553 |
This theorem is referenced by: falimd 1558 tbw-bijust 1698 tbw-negdf 1699 tbw-ax4 1703 merco1 1713 merco2 1736 ab0w 4378 csbprc 4408 ralf0 4513 ralnralall 4514 tgcgr4 28529 frgrregord013 30404 nalfal 36382 imsym1 36397 consym1 36399 dissym1 36400 unisym1 36402 exisym1 36403 subsym1 36406 bj-falor2 36564 bj-prmoore 37094 wl-2mintru2 37470 orfa1 38070 orfa2 38071 bifald 38072 botel 38089 lindslinindsimp2 48353 |
Copyright terms: Public domain | W3C validator |