Variable rule in dependent type theory
Essentially, $\Gamma$ is a store that maps variables to types. 

This rule says that we can deduce that a variable has a type in a context if that type is stored for our variable in the context. 

The rule is deliberately simple, and is a base case for the inductive process that is type derivation. 

In short, to check the type of a variable, just look it up in the environment.