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

Theorem fal 1553
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 1543 . . 3
21notnoti 143 . 2 ¬ ¬ ⊤
3 df-fal 1552 . 2 (⊥ ↔ ¬ ⊤)
42, 3mtbir 323 1 ¬ ⊥
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wtru 1540  wfal 1551
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 207  df-tru 1542  df-fal 1552
This theorem is referenced by:  nbfal  1554  bifal  1555  falim  1556  dfnot  1558  notfal  1567  falantru  1574  nffal  1804  alfal  1807  sbn1  2106  nonconne  2951  dfnul3  4336  noel  4337  vn0  4344  csbprc  4408  axnulALT  5303  axnul  5304  canthp1  10695  rlimno1  15691  1stccnp  23471  axsepg2ALT  35098  nexfal  36407  negsym1  36419  nandsym1  36424  bj-falor  36586  orfa  38090  fald  38137  dihglblem6  41343  ifpdfan  43484  ifpnot  43488  ifpid2  43489  ifpdfxor  43505
  Copyright terms: Public domain W3C validator