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 ¬

Proof

Step Hyp Ref Expression
1 tru
2 1 notnoti ¬ ¬
3 df-fal ¬
4 2 3 mtbir ¬