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

Theorem fal 1459
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 1456 . . 3  |- T.
21notnoti 127 . 2  |-  -.  -. T.
3 df-fal 1458 . 2  |-  ( F.  <->  -. T.  )
42, 3mtbir 306 1  |-  -. F.
Colors of variables: wff setvar class
Syntax hints:   -. wn 3   T. wtru 1453   F. wfal 1457
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 190  df-tru 1455  df-fal 1458
This theorem is referenced by:  nbfal  1463  bifal  1465  falim  1466  dfnot  1470  falantru  1476  notfal  1487  nffal  1688  nonconne  2655  csbprc  3774  axnulALT  4524  axnul  4525  canthp1  9097  rlimno1  13794  1stccnp  20554  rusgra0edg  25762  alnof  31133  nextf  31137  negsym1  31148  nandsym1  31153  subsym1  31158  bj-falor  31232  bj-nffal  31265  orfa  32379  fald  32435  dihglblem6  34979  ifpdfan  36180  ifpnot  36184  ifpid2  36185  ifpdfxor  36202
  Copyright terms: Public domain W3C validator