HOLE Home Higher-Order Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HOLE Home  >  Th. List  >  wnot Unicode version
Theorem wnot 128
Description: Negation type.
Assertion
Ref Expression
wnot |- ~ :(* -> *)
Proof of Theorem wnot
Dummy variable p is distinct from all other variables.
StepHypRef Expression
1 wim 127 . . . 4 |- ==> :(* -> (* -> *))
2 wv 58 . . . 4 |- p:*:*
3 wfal 125 . . . 4 |- F.:*
41, 2, 3wov 64 . . 3 |- [p:* ==> F.]:*
54wl 59 . 2 |- \p:* [p:* ==> F.]:(* -> *)
6 df-not 120 . 2 |- T. |= [~ = \p:* [p:* ==> F.]]
75, 6eqtypri 71 1 |- ~ :(* -> *)
Colors of variables: type var term
Syntax hints:  tv 1   -> ht 2  *hb 3  \kl 6  T.kt 8  [kbr 9  wffMMJ2t 12  F.tfal 108  ~ tne 110   ==> tim 111
This theorem was proved from axioms:  ax-cb1 29  ax-refl 39
This theorem depends on definitions:  df-al 116  df-fal 117  df-an 118  df-im 119  df-not 120
This theorem is referenced by:  notval  135  notval2  149  notnot1  150  con3d  152  alnex  174  exnal1  175  exmid  186  notnot  187  exnal  188  ax3  192  ax6  195  ax9  199  ax12  202
  Copyright terms: Public domain W3C validator