HOLE Home Higher-Order Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HOLE Home  >  Th. List  >  df-not Structured version   Unicode version

Definition df-not 120
Description: Define the negation operator.
Assertion
Ref Expression
df-not |- T. |= [~ = \p:* [p:* ==> F.]]

Detailed syntax breakdown of Definition df-not
StepHypRef Expression
1 kt 8 . 2 term T.
2 tne 110 . . 3 term ~
3 hb 3 . . . 4 type *
4 vp . . . 4 var p
53, 4tv 1 . . . . 5 term p:*
6 tfal 108 . . . . 5 term F.
7 tim 111 . . . . 5 term ==>
85, 6, 7kbr 9 . . . 4 term [p:* ==> F.]
93, 4, 8kl 6 . . 3 term \p:* [p:* ==> F.]
10 ke 7 . . 3 term =
112, 9, 10kbr 9 . 2 term [~ = \p:* [p:* ==> F.]]
121, 11wffMMJ2 11 1 wff T. |= [~ = \p:* [p:* ==> F.]]
Colors of variables: type var term
This definition is referenced by:  wnot  128  notval  135
  Copyright terms: Public domain W3C validator