Theorem wnot 128

Description: Negation type.

Assertion

Ref	Expression
wnot	|- ~ :(* -> *)

Proof of Theorem wnot

Dummy variable p is distinct from all other variables.

Step	Hyp	Ref	Expression
1		wim 127	. . . 4 |- ==> :(* -> (* -> *))
2		wv 58	. . . 4 |- p:*:*
3		wfal 125	. . . 4 |- F.:*
4	1, 2, 3	wov 64	. . 3 |- [p:* ==> F.]:*
5	4	wl 59	. 2 |- \p:* [p:* ==> F.]:(* -> *)
6		df-not 120	. 2 |- T. |= [~ = \p:* [p:* ==> F.]]
7	5, 6	eqtypri 71	1 |- ~ :(* -> *)

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