Metamath Proof Explorer

Theorem bj-fal

Description: Shortening of fal using bj-mt2bi . (Contributed by Anthony Hart, 22-Oct-2010) (Proof shortened by Mel L. O'Cat, 11-Mar-2012) (Proof modification is discouraged.)

Ref Expression
Assertion bj-fal 
|- -. F.

Proof

Step Hyp Ref Expression
1 tru 
 |-  T.
2 df-fal 
 |-  ( F. <-> -. T. )
3 1 2 bj-mt2bi 
 |-  -. F.