Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > fal | Structured version Visualization version GIF version |
Description: The truth value ⊥ is refutable. (Contributed by Anthony Hart, 22-Oct-2010.) (Proof shortened by Mel L. O'Cat, 11-Mar-2012.) |
Ref | Expression |
---|---|
fal | ⊢ ¬ ⊥ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | tru 1532 | . . 3 ⊢ ⊤ | |
2 | 1 | notnoti 145 | . 2 ⊢ ¬ ¬ ⊤ |
3 | df-fal 1541 | . 2 ⊢ (⊥ ↔ ¬ ⊤) | |
4 | 2, 3 | mtbir 324 | 1 ⊢ ¬ ⊥ |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ⊤wtru 1529 ⊥wfal 1540 |
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 208 df-tru 1531 df-fal 1541 |
This theorem is referenced by: nbfal 1543 bifal 1544 falim 1545 dfnot 1547 notfal 1556 falantru 1563 nffal 1797 alfal 1800 nonconne 3028 csbprc 4357 axnulALT 5200 axnul 5201 canthp1 10065 rlimno1 15000 1stccnp 22000 nexfal 33651 negsym1 33663 nandsym1 33668 subsym1 33673 bj-falor 33816 orfa 35243 fald 35290 dihglblem6 38358 sbn1 38983 ifpdfan 39711 ifpnot 39715 ifpid2 39716 ifpdfxor 39733 |
Copyright terms: Public domain | W3C validator |