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

Theorem fal 1386
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 1383 . . 3  |- T.
21notnoti 123 . 2  |-  -.  -. T.
3 df-fal 1385 . 2  |-  ( F.  <->  -. T.  )
42, 3mtbir 299 1  |-  -. F.
Colors of variables: wff setvar class
Syntax hints:   -. wn 3   T. wtru 1380   F. wfal 1384
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 1382  df-fal 1385
This theorem is referenced by:  nbfal  1390  bifal  1392  falim  1393  dfnot  1398  falantru  1405  notfal  1416  nonconne  2675  csbprc  3821  axnulALT  4574  canthp1  9028  rlimno1  13435  1stccnp  19729  rusgra0edg  24631  alnof  29444  nextf  29448  negsym1  29459  nandsym1  29464  subsym1  29469  orfa  30082  fald  30140  bj-falor  33254  bj-nffal  33284  bj-nffal2  33285  dihglblem6  36137
  Copyright terms: Public domain W3C validator