The following puzzle is given in A Cartoon Guide to Lob's Theorem:
The Deduction Theorem states that whenever assuming a hypothesis H enables us to prove a formula F in classical logic, then (H->F) is a theorem in classical logic.
Let ◻Z stand for the proposition "Z is provable". Löb's Theorem shows that, whenever we have ((◻C)->C), we can prove C.
[Edit per suggestion by @NicolinoWill]: There are two hidden boxes in the above statement. One goes in place of "we have," and the other in place of "we can prove." So the statement in full rigorousness is $ \square ((\square C)\rightarrow C) \rightarrow\square C.$ This question is a great example to underscore the distinction between a statement made inside a system (object language) and statements humans make about such statements (metalanguage) since it is easy to conflate the two leading to perplexing and erroneous results.
Applying the Deduction Theorem to Löb's Theorem gives us, for all C: ((◻C)->C)->C
However, those familiar with the logic of material implication will realize that (X->Y)->Y implies (not X)->Y
Applied to the above, this yields (not ◻C)->C. That is, all statements which lack proofs are true.
The resolution of the paradox is recognizing the omission of the provability predicate - $\square$ - in both the antecedent and the consequent. At that point it no longer fits the axiom schema $[(X \rightarrow Y) \rightarrow Y] \rightarrow [\neg X \rightarrow Y]$, so the deduction theorem is inapplicable. Please feel free to comment on my analysis and whether you agree.