Theorem wfal 135

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

Assertion

Ref	Expression
wfal	⊢ ⊥:∗

Proof of Theorem wfal

Dummy variable p is distinct from all other variables.

Step	Hyp	Ref	Expression
1		wal 134	. . 3 ⊢ ∀:((∗ → ∗) → ∗)
2		wv 64	. . . 4 ⊢ p:∗:∗
3	2	wl 66	. . 3 ⊢ λp:∗ p:∗:(∗ → ∗)
4	1, 3	wc 50	. 2 ⊢ (∀λp:∗ p:∗):∗
5		df-fal 127	. 2 ⊢ ⊤⊧[⊥ = (∀λp:∗ p:∗)]
6	4, 5	eqtypri 81	1 ⊢ ⊥:∗

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