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

Theorem fal 1332
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 1331 . . 3  |-  T.
21notnoti 118 . 2  |-  -.  -.  T.
3 df-fal 1330 . 2  |-  (  F.  <->  -.  T.  )
42, 3mtbir 292 1  |-  -.  F.
Colors of variables: wff set class
Syntax hints:   -. wn 3    T. wtru 1326    F. wfal 1327
This theorem is referenced by:  nbfal  1335  bifal  1337  falim  1338  falantru  1348  notfal  1359  axnulALT  4337  canthp1  8530  rlimno1  12448  1stccnp  17526  alnof  26153  nextf  26157  negsym1  26168  nandsym1  26173  subsym1  26178  dihglblem6  32139
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 179  df-tru 1329  df-fal 1330
  Copyright terms: Public domain W3C validator