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

Theorem wim 137
Description: Implication type. (Contributed by Mario Carneiro, 8-Oct-2014.)
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 136 . . . . . 6 |- /\ :(* -> (* -> *))
2 wv 64 . . . . . 6 |- p:*:*
3 wv 64 . . . . . 6 |- q:*:*
41, 2, 3wov 72 . . . . 5 |- [p:* /\ q:*]:*
54, 2weqi 76 . . . 4 |- [[p:* /\ q:*] = p:*]:*
65wl 66 . . 3 |- \q:* [[p:* /\ q:*] = p:*]:(* -> *)
76wl 66 . 2 |- \p:* \q:* [[p:* /\ q:*] = p:*]:(* -> (* -> *))
8 df-im 129 . 2 |- T. |= [ ==> = \p:* \q:* [[p:* /\ q:*] = p:*]]
97, 8eqtypri 81 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 119   ==> tim 121
This theorem was proved from axioms:  ax-cb1 29  ax-weq 40  ax-refl 42  ax-wv 63  ax-wl 65  ax-wov 71  ax-eqtypri 80
This theorem depends on definitions:  df-an 128  df-im 129
This theorem is referenced by:  wnot  138  wex  139  wor  140  exval  143  notval  145  imval  146  orval  147  notval2  159  ecase  163  olc  164  orc  165  exlimdv2  166  exlimdv  167  ax4e  168  exlimd  183  ac  197  ax2  204  ax3  205  ax5  207  ax11  214  axrep  220  axpow  221  axun  222
  Copyright terms: Public domain W3C validator