![]() |
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 1527 | . . 3 ⊢ ⊤ | |
2 | 1 | notnoti 137 | . 2 ⊢ ¬ ¬ ⊤ |
3 | df-fal 1529 | . 2 ⊢ (⊥ ↔ ¬ ⊤) | |
4 | 2, 3 | mtbir 312 | 1 ⊢ ¬ ⊥ |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ⊤wtru 1524 ⊥wfal 1528 |
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 197 df-tru 1526 df-fal 1529 |
This theorem is referenced by: nbfal 1535 bifal 1537 falim 1538 dfnot 1542 falantru 1548 notfal 1559 nffal 1772 nonconne 2835 csbprc 4013 csbprcOLD 4014 axnulALT 4820 axnul 4821 canthp1 9514 rlimno1 14428 1stccnp 21313 alnof 32526 nextf 32530 negsym1 32541 nandsym1 32546 subsym1 32551 bj-falor 32694 orfa 34011 fald 34066 dihglblem6 36946 ifpdfan 38127 ifpnot 38131 ifpid2 38132 ifpdfxor 38149 |
Copyright terms: Public domain | W3C validator |