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

Definition df-im 129
Description: Define the implication operator. (Contributed by Mario Carneiro, 8-Oct-2014.)
Assertion
Ref Expression
df-im |- T. |= [ ==> = \p:* \q:* [[p:* /\ q:*] = p:*]]
Distinct variable group:   p,q

Detailed syntax breakdown of Definition df-im
StepHypRef Expression
1 kt 8 . 2 term T.
2 tim 121 . . 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 119 . . . . . . 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 T. |= [ ==> = \p:* \q:* [[p:* /\ q:*] = p:*]]
Colors of variables: type var term
This definition is referenced by:  wim  137  imval  146
  Copyright terms: Public domain W3C validator