Theorem wfal 125

Description: Contradiction type.

Assertion

Ref	Expression
wfal	|- F.:*

Proof of Theorem wfal

Dummy variable p is distinct from all other variables.

Step	Hyp	Ref	Expression
1		wal 124	. . 3 |- A.:((* -> *) -> *)
2		wv 58	. . . 4 |- p:*:*
3	2	wl 59	. . 3 |- \p:* p:*:(* -> *)
4	1, 3	wc 45	. 2 |- (A.\p:* p:*):*
5		df-fal 117	. 2 |- T. |= [F. = (A.\p:* p:*)]
6	4, 5	eqtypri 71	1 |- F.:*

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

This theorem was proved from axioms:  ax-cb1 29  ax-refl 39

This theorem depends on definitions:  df-al 116  df-fal 117

This theorem is referenced by:  wnot  128  notval  135  pm2.21  143  notval2  149  notnot1  150  con2d  151  alnex  174  exmid  186  notnot  187  ax3  192