HOLE Home Higher-Order Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HOLE Home  >  Th. List  >  wfal Unicode version
Theorem wfal 125
Description: Contradiction type.
Assertion
Ref Expression
wfal |- F.:*
Proof of Theorem wfal
Dummy variable p is distinct from all other variables.
StepHypRef Expression
1 wal 124 . . 3 |- A.:((* -> *) -> *)
2 wv 58 . . . 4 |- p:*:*
32wl 59 . . 3 |- \p:* p:*:(* -> *)
41, 3wc 45 . 2 |- (A.\p:* p:*):*
5 df-fal 117 . 2 |- T. |= [F. = (A.\p:* p:*)]
64, 5eqtypri 71 1 |- F.:*
Colors of variables: type var term
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
  Copyright terms: Public domain W3C validator