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

Theorem fal 1556
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 1546 . . 3
21notnoti 143 . 2 ¬ ¬ ⊤
3 df-fal 1555 . 2 (⊥ ↔ ¬ ⊤)
42, 3mtbir 323 1 ¬ ⊥
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wtru 1543  wfal 1554
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 206  df-tru 1545  df-fal 1555
This theorem is referenced by:  nbfal  1557  bifal  1558  falim  1559  dfnot  1561  notfal  1570  falantru  1577  nffal  1808  alfal  1811  sbn1  2106  nonconne  2956  dfnul3  4291  noel  4295  vn0  4303  csbprc  4371  axnulALT  5266  axnul  5267  canthp1  10597  rlimno1  15545  1stccnp  22829  nexfal  34906  negsym1  34918  nandsym1  34923  bj-falor  35078  orfa  36570  fald  36617  dihglblem6  39832  ifpdfan  41812  ifpnot  41816  ifpid2  41817  ifpdfxor  41833
  Copyright terms: Public domain W3C validator