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

Theorem fal 1631
 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 1628 . . 3
21notnoti 137 . 2 ¬ ¬ ⊤
3 df-fal 1630 . 2 (⊥ ↔ ¬ ⊤)
42, 3mtbir 312 1 ¬ ⊥
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3  ⊤wtru 1625  ⊥wfal 1629 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 197  df-tru 1627  df-fal 1630 This theorem is referenced by:  nbfal  1636  bifal  1638  falim  1639  dfnot  1643  falantru  1649  notfal  1660  nffal  1873  nonconne  2936  csbprc  4115  csbprcOLD  4116  axnulALT  4931  axnul  4932  canthp1  9660  rlimno1  14575  1stccnp  21459  alnof  32699  nextf  32703  negsym1  32714  nandsym1  32719  subsym1  32724  bj-falor  32867  orfa  34186  fald  34241  dihglblem6  37123  ifpdfan  38304  ifpnot  38308  ifpid2  38309  ifpdfxor  38326
 Copyright terms: Public domain W3C validator