|   | 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 1543 | . . 3 ⊢ ⊤ | |
| 2 | 1 | notnoti 143 | . 2 ⊢ ¬ ¬ ⊤ | 
| 3 | df-fal 1552 | . 2 ⊢ (⊥ ↔ ¬ ⊤) | |
| 4 | 2, 3 | mtbir 323 | 1 ⊢ ¬ ⊥ | 
| Colors of variables: wff setvar class | 
| Syntax hints: ¬ wn 3 ⊤wtru 1540 ⊥wfal 1551 | 
| 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 1542 df-fal 1552 | 
| This theorem is referenced by: nbfal 1554 bifal 1555 falim 1556 dfnot 1558 notfal 1567 falantru 1574 nffal 1804 alfal 1807 sbn1 2106 nonconne 2951 dfnul3 4336 noel 4337 vn0 4344 csbprc 4408 axnulALT 5303 axnul 5304 canthp1 10695 rlimno1 15691 1stccnp 23471 axsepg2ALT 35098 nexfal 36407 negsym1 36419 nandsym1 36424 bj-falor 36586 orfa 38090 fald 38137 dihglblem6 41343 ifpdfan 43484 ifpnot 43488 ifpid2 43489 ifpdfxor 43505 | 
| Copyright terms: Public domain | W3C validator |