My favorite application of the Axiom of Choice, which Computer Scientists will appreciate:

Theorem ("Konig's Lemma"): If a tree has infinitely many nodes, and every node has only finitely many children, then the tree must have an infinite branch.

Proof: The tree's root, X1, has infinitely many descendants. Since the root has only finitely many children, some child, X2, of the root, must have infinitely many descendants. Since X2 has only finitely many children, some child, X3, of X2, must have infinitely many descendants. This process repeats forever, producing a sequence X1, X2, X3, ... which is an infinite branch through the tree.