Theorem wfal 125

Description: Contradiction type.

Assertion

Ref	Expression
wfal	⊢ ⊥:∗

Proof of Theorem wfal

Dummy variable p is distinct from all other variables.

Step	Hyp	Ref	Expression
1		wal 124	. . 3 ⊢ ∀:((∗ → ∗) → ∗)
2		wv 58	. . . 4 ⊢ p:∗:∗
3	2	wl 59	. . 3 ⊢ λp:∗ p:∗:(∗ → ∗)
4	1, 3	wc 45	. 2 ⊢ (∀λp:∗ p:∗):∗
5		df-fal 117	. 2 ⊢ ⊤⊧[⊥ = (∀λp:∗ p:∗)]
6	4, 5	eqtypri 71	1 ⊢ ⊥:∗

Syntax hints:  tv 1   → ht 2  ∗hb 3  kc 5  λkl 6  ⊤kt 8  wffMMJ2t 12  ⊥tfal 108  ∀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