Theorem wnot 138

Description: Negation type. (Contributed by Mario Carneiro, 8-Oct-2014.)

Assertion

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

Proof of Theorem wnot

Dummy variable p is distinct from all other variables.

Step	Hyp	Ref	Expression
1		wim 137	. . . 4 |- ==> :(* -> (* -> *))
2		wv 64	. . . 4 |- p:*:*
3		wfal 135	. . . 4 |- F.:*
4	1, 2, 3	wov 72	. . 3 |- [p:* ==> F.]:*
5	4	wl 66	. 2 |- \p:* [p:* ==> F.]:(* -> *)
6		df-not 130	. 2 |- T. |= [~ = \p:* [p:* ==> F.]]
7	5, 6	eqtypri 81	1 |- ~ :(* -> *)

Syntax hints:  tv 1   -> ht 2  *hb 3  \kl 6  T.kt 8  [kbr 9  wffMMJ2t 12  F.tfal 118  ~ tne 120   ==> tim 121

This theorem was proved from axioms:  ax-cb1 29  ax-weq 40  ax-refl 42  ax-wc 49  ax-wv 63  ax-wl 65  ax-wov 71  ax-eqtypri 80

This theorem depends on definitions:  df-al 126  df-fal 127  df-an 128  df-im 129  df-not 130

This theorem is referenced by:  notval  145  notval2  159  notnot1  160  con3d  162  alnex  186  exnal1  187  exmid  199  notnot  200  exnal  201  ax3  205  ax6  208  ax9  212  ax12  215