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

Theorem wim 127
Description: Implication type.
Assertion
Ref Expression
wim |- ==> :(* -> (* -> *))

Proof of Theorem wim
Dummy variables p q are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 wan 126 . . . . . 6 |- /\ :(* -> (* -> *))
2 wv 58 . . . . . 6 |- p:*:*
3 wv 58 . . . . . 6 |- q:*:*
41, 2, 3wov 64 . . . . 5 |- [p:* /\ q:*]:*
54, 2weqi 68 . . . 4 |- [[p:* /\ q:*] = p:*]:*
65wl 59 . . 3 |- \q:* [[p:* /\ q:*] = p:*]:(* -> *)
76wl 59 . 2 |- \p:* \q:* [[p:* /\ q:*] = p:*]:(* -> (* -> *))
8 df-im 119 . 2 |- T. |= [ ==> = \p:* \q:* [[p:* /\ q:*] = p:*]]
97, 8eqtypri 71 1 |- ==> :(* -> (* -> *))
Colors of variables: type var term
Syntax hints:  tv 1   -> ht 2  *hb 3  \kl 6   = ke 7  T.kt 8  [kbr 9  wffMMJ2t 12   /\ tan 109   ==> tim 111
This theorem is referenced by:  wnot  128  wex  129  wor  130  exval  133  notval  135  imval  136  orval  137  notval2  149  ecase  153  olc  154  orc  155  exlimdv2  156  exlimdv  157  ax4e  158  exlimd  171  ac  184  ax2  191  ax3  192  ax5  194  ax11  201  axrep  207  axpow  208  axun  209
This theorem was proved from axioms:  ax-cb1 29  ax-refl 39
This theorem depends on definitions:  df-an 118  df-im 119
  Copyright terms: Public domain W3C validator