Erdosde Bruijn theorem: An (infinite) graph G is kcolorable iff every finite subgraph is kcolorable.
I will sketch the proof for the case where G is countable. We can assume the vertices are {1,2,3,...}. Let COL_{i} be a kcoloring of G restricted to {1,...,i}. We will use the COL_{i}'s to obtain a kcoloring of the entire graph G. We can assume the COL_{i}'s use colors {1,...,k} so we can speak of the least color j such that blah blah.
We color node 1 by the least color that an infinite number of the COL_{i}'s color 1. Then REMOVE all of the COL_{i}'s that do not use that color on 1. (We kill all those that disagree with us! as I told my students.) Note that there are still an infinite number of COL_{i}'s left.
We color node 2 by the least color that an infinite number of the COL_{i}'s THAT ARE LEFT color 2. Then REMOVE all of the COL_{i}'s that do not use that color on 2. Note that there are still an infinite number of COL_{i}'s left.
And so on.
End of Sketch of Proof.

This type of argument can be used to proof the following:
 If we already have the infinite Ramsey Theorem on N, we can obtain the finite Ramsey Theorem and (with a small trick) the Large Ramsey Theorem.
 If we already have the finite dilworth theorem (any FINITE partial order of width w can be covered with w chains) then we can obtain the infinite version of Dilworth's theorem: if an INFINITE partial order has width w can be covered with w chains.
 The method is called compactness argument and is very general. It is related to topological compactness, but I won't to into that here. (If a reader has a short explanation or pointer, please post.)

The method is noneffective in that if you are given a Turing machine that
tells you, for all i,j, COL_{i}(j), then the proof does not appear
to be able to give you a Turing machine for a coloring of G.
There are two ways this has been formalized, though I list three since
the third one strengthens the second one.
(For details see my survey of recursive combinatorics
here.)
 (Bean, 1976) There is a computable graph (Vertex set N, Edge set decidable) that is 3colorable but there is no computable finite coloring whatsoever. (He also made the graph planar, which was not needed but nice.)
 (Carstens and Pappinghaus, 1983) For every k ≥ 3 There is a highly computable graph (Vertex set N, the function that, given a graph, outputs its finite set of neighbors is computable) that is kcolorable but not computably kcolorable. (NOTE: if a highly comp. graph is kcol then IT IS computably 2k1 colorable.)
 (Schmerl, 1980) For every k ≥3 There is a highly computable graph (Vertex set N, the function that, given a graph, outputs its finite set of neighbors is computable) that is kcolorable but not computably (2k2)colorable.