Metamath Proof Explorer

Definition df-fal

Description: Definition of the truth value "false", or "falsum", denoted by F. . See also df-tru . (Contributed by Anthony Hart, 22-Oct-2010)

Ref Expression
Assertion df-fal 
|- ( F. <-> -. T. )

Detailed syntax breakdown

Step Hyp Ref Expression
0 wfal 
 |-  F.
1 wtru 
 |-  T.
2 1 wn 
 |-  -. T.
3 0 2 wb 
 |-  ( F. <-> -. T. )