![]() |
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 1628 | . . 3 ⊢ ⊤ | |
2 | 1 | notnoti 137 | . 2 ⊢ ¬ ¬ ⊤ |
3 | df-fal 1630 | . 2 ⊢ (⊥ ↔ ¬ ⊤) | |
4 | 2, 3 | mtbir 312 | 1 ⊢ ¬ ⊥ |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ⊤wtru 1625 ⊥wfal 1629 |
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 1627 df-fal 1630 |
This theorem is referenced by: nbfal 1636 bifal 1638 falim 1639 dfnot 1643 falantru 1649 notfal 1660 nffal 1873 nonconne 2936 csbprc 4115 csbprcOLD 4116 axnulALT 4931 axnul 4932 canthp1 9660 rlimno1 14575 1stccnp 21459 alnof 32699 nextf 32703 negsym1 32714 nandsym1 32719 subsym1 32724 bj-falor 32867 orfa 34186 fald 34241 dihglblem6 37123 ifpdfan 38304 ifpnot 38308 ifpid2 38309 ifpdfxor 38326 |
Copyright terms: Public domain | W3C validator |