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

Theorem fal 1402
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 1399 . . 3
21notnoti 123 . 2
3 df-fal 1401 . 2
42, 3mtbir 299 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3   wtru 1396   wfal 1400
This theorem is referenced by:  nbfal  1406  bifal  1408  falim  1409  dfnot  1414  falantru  1421  notfal  1432  nffal  1629  nonconne  2665  csbprc  3821  axnulALT  4579  canthp1  9053  rlimno1  13476  1stccnp  19963  rusgra0edg  24955  alnof  29867  nextf  29871  negsym1  29882  nandsym1  29887  subsym1  29892  orfa  30479  fald  30536  bj-falor  34173  bj-nffal  34201  dihglblem6  37067  bj-ifid2  37711  bj-ifnot  37717  bj-ifdfan  37727  bj-ifdfxor  37732
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 185  df-tru 1398  df-fal 1401
  Copyright terms: Public domain W3C validator