Higher-Order Logic Explorer		< Previous   Next > Nearby theorems
Mirrors  >  Home  >  HOLE Home  >  Th. List  >  wnot		GIF version

---

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 ⊢ ⊥:∗
4	1, 2, 3	wov 64	. . 3 ⊢ [p:∗ ⇒ ⊥]:∗
5	4	wl 59	. 2 ⊢ λp:∗ [p:∗ ⇒ ⊥]:(∗ → ∗)
6		df-not 120	. 2 ⊢ ⊤⊧[¬ = λp:∗ [p:∗ ⇒ ⊥]]
7	5, 6	eqtypri 71	1 ⊢ ¬ :(∗ → ∗)

Colors of variables: type var term

Syntax hints:  tv 1   → ht 2  ∗hb 3  λkl 6  ⊤kt 8  [kbr 9  wffMMJ2t 12  ⊥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