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

Theorem fal 1482
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 1479 . . 3
21notnoti 136 . 2 ¬ ¬ ⊤
3 df-fal 1481 . 2 (⊥ ↔ ¬ ⊤)
42, 3mtbir 312 1 ¬ ⊥
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wtru 1476  wfal 1480
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 196  df-tru 1478  df-fal 1481
This theorem is referenced by:  nbfal  1486  bifal  1488  falim  1489  dfnot  1493  falantru  1499  notfal  1510  nffal  1723  nonconne  2794  csbprc  3932  csbprcOLD  3933  axnulALT  4710  axnul  4711  canthp1  9333  rlimno1  14181  1stccnp  21023  rusgra0edg  26276  alnof  31365  nextf  31369  negsym1  31380  nandsym1  31385  subsym1  31390  bj-falor  31536  bj-nffal  31569  orfa  32845  fald  32900  dihglblem6  35441  ifpdfan  36623  ifpnot  36627  ifpid2  36628  ifpdfxor  36645
  Copyright terms: Public domain W3C validator