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

Theorem fal 1313
Description:  F. is not provable. (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 1312 . . 3  |-  T.
21notnoti 115 . 2  |-  -.  -.  T.
3 df-fal 1311 . 2  |-  (  F.  <->  -.  T.  )
42, 3mtbir 290 1  |-  -.  F.
Colors of variables: wff set class
Syntax hints:   -. wn 3    T. wtru 1307    F. wfal 1308
This theorem is referenced by:  nbfal  1316  bifal  1318  falim  1319  truanfal  1327  falantru  1328  notfal  1339  axnulALT  4147  canthp1  8276  rlimno1  12127  1stccnp  17188  alnof  24841  nextf  24845  negsym1  24856  nandsym1  24861  subsym1  24866  dihglblem6  31530
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-tru 1310  df-fal 1311
  Copyright terms: Public domain W3C validator