HOLE Home Higher-Order Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HOLE Home  >  Th. List  >  df-im GIF version

Definition df-im 119
Description: Define the implication operator.
Assertion
Ref Expression
df-im ⊤⊧[ ⇒ = λp:∗ λq:∗ [[p:∗ q:∗] = p:∗]]
Distinct variable group:   p,q

Detailed syntax breakdown of Definition df-im
StepHypRef Expression
1 kt 8 . 2 term
2 tim 111 . . 3 term
3 hb 3 . . . 4 type
4 vp . . . 4 var p
5 vq . . . . 5 var q
63, 4tv 1 . . . . . . 7 term p:∗
73, 5tv 1 . . . . . . 7 term q:∗
8 tan 109 . . . . . . 7 term
96, 7, 8kbr 9 . . . . . 6 term [p:∗ q:∗]
10 ke 7 . . . . . 6 term =
119, 6, 10kbr 9 . . . . 5 term [[p:∗ q:∗] = p:∗]
123, 5, 11kl 6 . . . 4 term λq:∗ [[p:∗ q:∗] = p:∗]
133, 4, 12kl 6 . . 3 term λp:∗ λq:∗ [[p:∗ q:∗] = p:∗]
142, 13, 10kbr 9 . 2 term [ ⇒ = λp:∗ λq:∗ [[p:∗ q:∗] = p:∗]]
151, 14wffMMJ2 11 1 wff ⊤⊧[ ⇒ = λp:∗ λq:∗ [[p:∗ q:∗] = p:∗]]
Colors of variables: type var term
This definition is referenced by:  wim  127  imval  136
  Copyright terms: Public domain W3C validator