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

Theorem fal 1377
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 1374 . . 3  |- T.
21notnoti 123 . 2  |-  -.  -. T.
3 df-fal 1376 . 2  |-  ( F.  <->  -. T.  )
42, 3mtbir 299 1  |-  -. F.
Colors of variables: wff setvar class
Syntax hints:   -. wn 3   T. wtru 1371   F. wfal 1375
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 1373  df-fal 1376
This theorem is referenced by:  nbfal  1381  bifal  1383  falim  1384  dfnot  1389  falantru  1396  notfal  1407  csbprc  3757  axnulALT  4503  canthp1  8908  rlimno1  13219  1stccnp  19168  alnof  28368  nextf  28372  negsym1  28383  nandsym1  28388  subsym1  28393  orfa  29006  fald  29064  rusgra0edg  30697  bj-falor  32392  bj-nffal  32420  bj-nffal2  32421  dihglblem6  35267
  Copyright terms: Public domain W3C validator