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.

Step	Hyp	Ref	Expression
1		wan 126	. . . . . 6 ⊢ ∧ :(∗ → (∗ → ∗))
2		wv 58	. . . . . 6 ⊢ p:∗:∗
3		wv 58	. . . . . 6 ⊢ q:∗:∗
4	1, 2, 3	wov 64	. . . . 5 ⊢ [p:∗ ∧ q:∗]:∗
5	4, 2	weqi 68	. . . 4 ⊢ [[p:∗ ∧ q:∗] = p:∗]:∗
6	5	wl 59	. . 3 ⊢ λq:∗ [[p:∗ ∧ q:∗] = p:∗]:(∗ → ∗)
7	6	wl 59	. 2 ⊢ λp:∗ λq:∗ [[p:∗ ∧ q:∗] = p:∗]:(∗ → (∗ → ∗))
8		df-im 119	. 2 ⊢ ⊤⊧[ ⇒ = λp:∗ λq:∗ [[p:∗ ∧ q:∗] = p:∗]]
9	7, 8	eqtypri 71	1 ⊢ ⇒ :(∗ → (∗ → ∗))

Syntax hints:  tv 1   → ht 2  ∗hb 3  λkl 6   = ke 7  ⊤kt 8  [kbr 9  wffMMJ2t 12   ∧ tan 109   ⇒ tim 111

This theorem was proved from axioms:  ax-cb1 29  ax-refl 39

This theorem depends on definitions:  df-an 118  df-im 119

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