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

Theorem fal 1667
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 1657 . . 3
21notnoti 139 . 2 ¬ ¬ ⊤
3 df-fal 1666 . 2 (⊥ ↔ ¬ ⊤)
42, 3mtbir 314 1 ¬ ⊥
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wtru 1653  wfal 1665
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 198  df-tru 1656  df-fal 1666
This theorem is referenced by:  nbfal  1668  bifal  1669  falim  1670  dfnot  1672  notfal  1681  falantru  1688  nffal  1900  alfal  1903  nonconne  2949  csbprc  4144  axnulALT  4949  axnul  4950  canthp1  9731  rlimno1  14672  1stccnp  21548  nexfal  32847  negsym1  32858  nandsym1  32863  subsym1  32868  bj-falor  33008  orfa  34306  fald  34360  dihglblem6  37299  ifpdfan  38489  ifpnot  38493  ifpid2  38494  ifpdfxor  38511
  Copyright terms: Public domain W3C validator