a mathematical system cannot assert its own soundness without becoming inconsistent [Yudkowsky]
if $PA\vdash$ $Bew$(#P) $\rightarrow P)$, then $PA\vdash P$
where $Bew$(#P) means that the formula $P$ with Gödel number #P is provable.
Other than Leon Henkin's application to show that Santa Claus exists (also see here), Michael Detlefsen wrote about limitations of mechanism which I do not have a copy but I did read through a refutation of it here. (Note: The first page of Detlefsen's paper can be accessed here).
Additionally, Drucker mentions Kripke's 1967 "new proof" of the theorem here.
My question is has there been any other interesting non-trivial applications of the theorem other than the cited ones?