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

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.
StepHypRef Expression
1 wal 134 . . 3 :((∗ → ∗) → ∗)
2 wv 64 . . . 4 p:∗:∗
32wl 66 . . 3 λp:∗ p:∗:(∗ → ∗)
41, 3wc 50 . 2 (λp:∗ p:∗):∗
5 df-fal 127 . 2 ⊤⊧[⊥ = (λp:∗ p:∗)]
64, 5eqtypri 81 1 ⊥:∗
 Colors of variables: type var term 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
 Copyright terms: Public domain W3C validator