Non-trivial consequences of Lob's theorem Informally, Löb's theorem (Wikipedia, PlanetMath) shows that:

a mathematical system cannot assert its own soundness without becoming inconsistent [Yudkowsky]

In symbols:

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?
 A: Löb's theorem can be used to show that there exist equilibria in games like prisoner's dilemma when the participants are computer programs that can read each other's source code.
If player 1 can show that player 2 will cooperate when given player 1's source code, and vice versa, then we can have an equilibrium. The catch is that player 2 needs to predict what will happen when its own source code is fed to player 1 and vice versa. So implicitly each player must reason about itself. Löb's theorem shows there is a consistent way to to this. See Robust Cooperation in the Prisoner's Dilemma: Program Equilibrium via Provability Logic.
It's not entirely practical but it's interesting anyway.
A: Löb's theorem provides the essential ingredient for a complete axiomatization of propositional provability logic.  In detail: Work with the usual notation of propositional modal logic, which has propositional variables, the usual Boolean connectives, and the unary modal operator $\square$.  The usual reading of $\square p$ is "necessarily $p$", but in provability logic, the intended reading is "it is provable that $p$."  Call a modal formula $\phi$ valid if PA proves all the sentences obtainable from $\phi$ by replacing its propositional variables by sentences of the language of PA and then replacing subformulas of the form $\square\alpha$ with $Bew(\sharp\alpha)$ (starting with the innermost $\square$ and working outward). Solovay showed that this notion of validity is identical to formal provability in an axiomatic system obtained by starting with the standard system K for what is called normal modal propositional logic, and adjoining the schema that formalizes Löb's theorem: $(\square(\square\alpha\to\alpha))\to\square\alpha$.  
