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

Theorem fal 1542
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 1532 . . 3
21notnoti 145 . 2 ¬ ¬ ⊤
3 df-fal 1541 . 2 (⊥ ↔ ¬ ⊤)
42, 3mtbir 324 1 ¬ ⊥
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wtru 1529  wfal 1540
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 208  df-tru 1531  df-fal 1541
This theorem is referenced by:  nbfal  1543  bifal  1544  falim  1545  dfnot  1547  notfal  1556  falantru  1563  nffal  1797  alfal  1800  nonconne  3028  csbprc  4357  axnulALT  5200  axnul  5201  canthp1  10065  rlimno1  15000  1stccnp  22000  nexfal  33651  negsym1  33663  nandsym1  33668  subsym1  33673  bj-falor  33816  orfa  35243  fald  35290  dihglblem6  38358  sbn1  38983  ifpdfan  39711  ifpnot  39715  ifpid2  39716  ifpdfxor  39733
  Copyright terms: Public domain W3C validator