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

Theorem fal 1444
Description: The truth value F. is refutable. (Contributed by Anthony Hart, 22-Oct-2010.) (Proof shortened by Mel L. O'Cat, 11-Mar-2012.)
Assertion
Ref Expression
fal  |-  -. F.

Proof of Theorem fal
StepHypRef Expression
1 tru 1441 . . 3  |- T.
21notnoti 126 . 2  |-  -.  -. T.
3 df-fal 1443 . 2  |-  ( F.  <->  -. T.  )
42, 3mtbir 300 1  |-  -. F.
Colors of variables: wff setvar class
Syntax hints:   -. wn 3   T. wtru 1438   F. wfal 1442
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 188  df-tru 1440  df-fal 1443
This theorem is referenced by:  nbfal  1448  bifal  1450  falim  1451  dfnot  1456  falantru  1463  notfal  1474  nffal  1676  nonconne  2632  csbprc  3798  axnulALT  4549  canthp1  9079  rlimno1  13702  1stccnp  20461  rusgra0edg  25666  alnof  31052  nextf  31056  negsym1  31067  nandsym1  31072  subsym1  31077  bj-falor  31157  bj-nffal  31185  orfa  32226  fald  32282  dihglblem6  34824  ifpdfan  36026  ifpnot  36030  ifpid2  36031  ifpdfxor  36048
  Copyright terms: Public domain W3C validator