My favorite proof is the one from Johnstone's Stone spaces because it works without the axiom of choice.

Someone is going to object to this, so I'll explain it right away: Tychonoff theorem says "product of compact spaces is compact" and not "product of compact spaces is compact and the definition of topological spaces is cast in stone and can never be changed".

My favorite proof is the one from Johnstone's Stone spaces for locales because it works without the axiom of choice.