Variable rule in dependent type theory This is the = Type variable rule that I'm seeing through out the my course and unable to grasp it completely. 

$$\dfrac{\phi \vdash \Gamma[\mathrm{ctx}] \qquad \Gamma(x) = \tau}
        {\phi; \Gamma \vdash x : \tau}
        \textsf{(ty-var)}$$ 

The first thing in antecedent looks like it's stating that $\Gamma$ is well-formed under the context $\phi$, is that right? What does the second thing in antecedent mean? I have a feeling of this but I am unable to get this simple rule.
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.