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 1547 | . . 3 ⊢ ⊤ | |
2 | 1 | notnoti 145 | . 2 ⊢ ¬ ¬ ⊤ |
3 | df-fal 1556 | . 2 ⊢ (⊥ ↔ ¬ ⊤) | |
4 | 2, 3 | mtbir 326 | 1 ⊢ ¬ ⊥ |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ⊤wtru 1544 ⊥wfal 1555 |
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 210 df-tru 1546 df-fal 1556 |
This theorem is referenced by: nbfal 1558 bifal 1559 falim 1560 dfnot 1562 notfal 1571 falantru 1578 nffal 1813 alfal 1816 sbn1 2109 nonconne 2951 dfnul3 4238 noel 4242 vn0 4250 csbprc 4318 axnulALT 5194 axnul 5195 canthp1 10265 rlimno1 15214 1stccnp 22356 nexfal 34328 negsym1 34340 nandsym1 34345 subsym1 34350 bj-falor 34500 orfa 35975 fald 36022 dihglblem6 39089 ifpdfan 40756 ifpnot 40760 ifpid2 40761 ifpdfxor 40777 |
Copyright terms: Public domain | W3C validator |