Dynamic testing of down casts as explained in TAPL
The first rule T-Typetest is a type-checking rule. Let's read it together. Firstly, $\Gamma$ is not important (on a first reading at least). We have the following premises:


$t_1$ has type $S$
if $x$ has type $T$ then $T_2$ has type $U$
$t_3$ has type $U$


The conclusions is, that we get an expression of type $U$ (I think your transcription should have "$: U$" instead of $\to t_3$ the conclusion):
$$\mathrm{if}\; t_1 \;\mathrm{in}\; T \;\mathrm{then}\; x \to t_2 \;\mathrm{else}\; t_3 \tag{1}$$
The meaning of this expression can be undrstood by looking at the other two rules, which are small-step operational semantics. Here is an incorrect explanation, which we will make correct in a moment:


If $t_1$ has type $T$ then (1) evaluates to $t_2$ with $x$ replaced by $t_1$. This is the case of "downcast", i.e., $t_1$ is downcast from $S$ to $T$, the downcast value is bound to $x$ and then $t_2$ is executed.
If $t_2$ does not have type $T$ then (1) evaluates to $t_3$. This is the "default" which we use when the downcast is not possible.


The above explanation is incorrect because we should use $v_1$ instead of $t_1$, by which the author is telling you: first evaluate $t_1$ to $v_1$, and then perform the downcast.

In an imaginary OO language the same thing might be written somewhat like this:

S t1 = ...;
...
if (t1 instanceof T) {
  T x = (T)t1;
  t2;
} else {
  t3;
}