A lesser known elementary theorem in basic proof theory is Löb’s Theorem. Even though I know it and know the basic idea of a proof for it, I cannot remember where I know this from, in the logic lectures I took it wasnt mentioned iirc, and in the introducting books I have read I cant remember it, too. And actually, I never needed it so far for anything, so I forgot about it.
The Löb Theorem basically states: If PA⊧ (⌈PA⊧A⌉→A) then PA⊧A.
Which reminds me of an old xkcd-comic.