Theorem fal 1490

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

Step	Hyp	Ref	Expression
1		tru 1487	. . 3 |- T.
2	1	notnoti 137	. 2 |- -. -. T.
3		df-fal 1489	. 2 |- ( F. <-> -. T. )
4	2, 3	mtbir 313	1 |- -. F.

Syntax hints:   -. wn 3   T. wtru 1484   F. wfal 1488

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 197  df-tru 1486  df-fal 1489

This theorem is referenced by:  nbfal  1495  bifal  1497  falim  1498  dfnot  1502  falantru  1508  notfal  1519  nffal  1732  nonconne  2806  csbprc  3980  csbprcOLD  3981  axnulALT  4787  axnul  4788  canthp1  9476  rlimno1  14384  1stccnp  21265  alnof  32401  nextf  32405  negsym1  32416  nandsym1  32421  subsym1  32426  bj-falor  32569  orfa  33881  fald  33936  dihglblem6  36629  ifpdfan  37810  ifpnot  37814  ifpid2  37815  ifpdfxor  37832