![]() |
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 1546 | . . 3 ⊢ ⊤ | |
2 | 1 | notnoti 143 | . 2 ⊢ ¬ ¬ ⊤ |
3 | df-fal 1555 | . 2 ⊢ (⊥ ↔ ¬ ⊤) | |
4 | 2, 3 | mtbir 323 | 1 ⊢ ¬ ⊥ |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ⊤wtru 1543 ⊥wfal 1554 |
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 1545 df-fal 1555 |
This theorem is referenced by: nbfal 1557 bifal 1558 falim 1559 dfnot 1561 notfal 1570 falantru 1577 nffal 1808 alfal 1811 sbn1 2106 nonconne 2956 dfnul3 4291 noel 4295 vn0 4303 csbprc 4371 axnulALT 5266 axnul 5267 canthp1 10597 rlimno1 15545 1stccnp 22829 nexfal 34906 negsym1 34918 nandsym1 34923 bj-falor 35078 orfa 36570 fald 36617 dihglblem6 39832 ifpdfan 41812 ifpnot 41816 ifpid2 41817 ifpdfxor 41833 |
Copyright terms: Public domain | W3C validator |