MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fal Structured version   Visualization version   GIF version

Theorem fal 1487
Description: The truth value is refutable. (Contributed by Anthony Hart, 22-Oct-2010.) (Proof shortened by Mel L. O'Cat, 11-Mar-2012.)
Assertion
Ref Expression
fal ¬ ⊥

Proof of Theorem fal
StepHypRef Expression
1 tru 1484 . . 3
21notnoti 137 . 2 ¬ ¬ ⊤
3 df-fal 1486 . 2 (⊥ ↔ ¬ ⊤)
42, 3mtbir 313 1 ¬ ⊥
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wtru 1481  wfal 1485
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 1483  df-fal 1486
This theorem is referenced by:  nbfal  1492  bifal  1494  falim  1495  dfnot  1499  falantru  1505  notfal  1516  nffal  1729  nonconne  2802  csbprc  3958  csbprcOLD  3959  axnulALT  4757  axnul  4758  canthp1  9436  rlimno1  14334  1stccnp  21205  alnof  32096  nextf  32100  negsym1  32111  nandsym1  32116  subsym1  32121  bj-falor  32264  orfa  33552  fald  33607  dihglblem6  36148  ifpdfan  37330  ifpnot  37334  ifpid2  37335  ifpdfxor  37352
  Copyright terms: Public domain W3C validator