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

Theorem fal 1388
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 1385 . . 3  |- T.
21notnoti 123 . 2  |-  -.  -. T.
3 df-fal 1387 . 2  |-  ( F.  <->  -. T.  )
42, 3mtbir 299 1  |-  -. F.
Colors of variables: wff setvar class
Syntax hints:   -. wn 3   T. wtru 1382   F. wfal 1386
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 1384  df-fal 1387
This theorem is referenced by:  nbfal  1392  bifal  1394  falim  1395  dfnot  1400  falantru  1407  notfal  1418  nffal  1614  nonconne  2649  csbprc  3804  axnulALT  4561  canthp1  9032  rlimno1  13452  1stccnp  19833  rusgra0edg  24824  alnof  29839  nextf  29843  negsym1  29854  nandsym1  29859  subsym1  29864  orfa  30451  fald  30508  bj-falor  33908  bj-nffal  33936  dihglblem6  36790
  Copyright terms: Public domain W3C validator