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

Theorem wim 127
 Description: Implication type.
Assertion
Ref Expression
wim

Proof of Theorem wim
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 wan 126 . . . . . 6
2 wv 58 . . . . . 6
3 wv 58 . . . . . 6
41, 2, 3wov 64 . . . . 5
54, 2weqi 68 . . . 4
65wl 59 . . 3
76wl 59 . 2
8 df-im 119 . 2
97, 8eqtypri 71 1
 Colors of variables: type var term Syntax hints:  tv 1   ht 2  hb 3  kl 6   ke 7  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