Metamath Proof Explorer

Theorem fal

Description: The truth value F. is refutable. (Contributed by Anthony Hart, 22-Oct-2010) (Proof shortened by Mel L. O'Cat, 11-Mar-2012)

Ref Expression
Assertion fal 
|- -. F.

Proof

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