Theorem wfal 135

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

Assertion

Ref	Expression
wfal	|- F.:*

Proof of Theorem wfal

Dummy variable p is distinct from all other variables.

Step	Hyp	Ref	Expression
1		wal 134	. . 3 |- A.:((* -> *) -> *)
2		wv 64	. . . 4 |- p:*:*
3	2	wl 66	. . 3 |- \p:* p:*:(* -> *)
4	1, 3	wc 50	. 2 |- (A.\p:* p:*):*
5		df-fal 127	. 2 |- T. |= [F. = (A.\p:* p:*)]
6	4, 5	eqtypri 81	1 |- F.:*

Syntax hints:  tv 1   -> ht 2  *hb 3  kc 5  \kl 6  T.kt 8  wffMMJ2t 12  F.tfal 118  A.tal 122

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

This theorem is referenced by:  wnot  138  notval  145  pm2.21  153  notval2  159  notnot1  160  con2d  161  alnex  186  exmid  199  notnot  200  ax3  205