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  4715  axnul  4716  canthp1  9355  rlimno1  14232  1stccnp  21075  rusgra0edg  26482  alnof  31571  nextf  31575  negsym1  31586  nandsym1  31591  subsym1  31596  bj-falor  31742  bj-nffal  31775  orfa  33051  fald  33106  dihglblem6  35647  ifpdfan  36829  ifpnot  36833  ifpid2  36834  ifpdfxor  36851
 Copyright terms: Public domain W3C validator