Some theorems are magical: their hypotheses are easy to meet, and when invoked (as lemmas) in the midst of an otherwise routine proof, they deliver the desired conclusion more or less straightaway—like pulling a rabbit from a hat. Here are five examples. Some are from outside of logic, but each is often useful within logic.
Baire Category Theorem. In any completely metrizable topological space, each nonempty open set is nonmeager.
Gödel's Diagonal Lemma. If a theory $T$ relatively interprets Robinson's arithmetic, then for each first order formula $\varphi(x,v_1,\dots,v_n)$ in the language of $T$, there is a $\psi(v_1,\dots,v_n)$ such that $T$ proves the sentence $\forall v_1 \dots \forall v_n[\psi(v_1,\dots,v_n) \leftrightarrow \varphi(\overline\psi,v_1,\dots,v_n)]$, where $\overline\psi$ is the code of $\psi$.
König's Tree Lemma. Every finitely splitting tree of infinite height has an infinite branch.
Knaster–Tarski Theorem. Every monotone nondecreasing operator on the powerset of a set has a fixed point.
Mostowski Collapsing Lemma. If $E$ is a well founded, set like, and extensional binary class relation on a class $M$, then there is a unique transitive class $N$ such that $(M, E)$ is isomorphic to $(N, \in)$.
Let's list other magical theorems that every logician can wield. Students among us will thereby learn of useful results that might otherwise escape their attention until much later. (There is related question here. But it and most of its answers don't focus on theorems useful in logic.) Please treat only one theorem per answer, and write as many answers as you like. Don't just link to Wikipedia or whatever; give a pithy statement. If possible, keep it informal. Bonus if the theorem isn't well known, or if you show it in action.
Best Answer
The Compactness Theorem
Funny that no one mentioned it so far. I find the Compactness Theorem magical, actually:
This let's you derive the finite form of Ramsey's theorem from the infinite form. That is magic. For most applications of this kind, the Compactness Theorem for propositional calculus is actually enough.
Compactness for first-order logic and propositional logic are actually equivalent (over ZF). In fact, there is a rather large collection of equivalent results:
The Compactness Theorem is strictly weaker than the Axiom of Choice, but it is not provable in plain ZF. This is often used to show that certain results are weaker than the Axiom of Choice. For example, it can be used to show that the existence of non-measurable sets is weaker than the Axiom of Choice (by an old result of Sierpiński).