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.

Step	Hyp	Ref	Expression
1		wan 136	. . . . . 6 |- /\ :(* -> (* -> *))
2		wv 64	. . . . . 6 |- p:*:*
3		wv 64	. . . . . 6 |- q:*:*
4	1, 2, 3	wov 72	. . . . 5 |- [p:* /\ q:*]:*
5	4, 2	weqi 76	. . . 4 |- [[p:* /\ q:*] = p:*]:*
6	5	wl 66	. . 3 |- \q:* [[p:* /\ q:*] = p:*]:(* -> *)
7	6	wl 66	. 2 |- \p:* \q:* [[p:* /\ q:*] = p:*]:(* -> (* -> *))
8		df-im 129	. 2 |- T. |= [ ==> = \p:* \q:* [[p:* /\ q:*] = p:*]]
9	7, 8	eqtypri 81	1 |- ==> :(* -> (* -> *))

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