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

Theorem fal 1552
 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 1542 . . 3
21notnoti 145 . 2 ¬ ¬ ⊤
3 df-fal 1551 . 2 (⊥ ↔ ¬ ⊤)
42, 3mtbir 326 1 ¬ ⊥
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3  ⊤wtru 1539  ⊥wfal 1550 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 210  df-tru 1541  df-fal 1551 This theorem is referenced by:  nbfal  1553  bifal  1554  falim  1555  dfnot  1557  notfal  1566  falantru  1573  nffal  1807  alfal  1810  nonconne  2999  csbprc  4316  axnulALT  5176  axnul  5177  canthp1  10083  rlimno1  15022  1stccnp  22108  nexfal  34013  negsym1  34025  nandsym1  34030  subsym1  34035  bj-falor  34182  orfa  35671  fald  35718  dihglblem6  38787  sbn1  39545  ifpdfan  40345  ifpnot  40349  ifpid2  40350  ifpdfxor  40366
 Copyright terms: Public domain W3C validator