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

Theorem fal 1313
Description:  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 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  4163  canthp1  8292  rlimno1  12143  1stccnp  17204  alnof  24913  nextf  24917  negsym1  24928  nandsym1  24933  subsym1  24938  dihglblem6  32152
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