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

Theorem fal 1530
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 1527 . . 3
21notnoti 137 . 2 ¬ ¬ ⊤
3 df-fal 1529 . 2 (⊥ ↔ ¬ ⊤)
42, 3mtbir 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