Variation on Lob's Theorem Lob's theorem is, of course, if $P(y)$ is a provability predicate for $S$, $S$ diagonalisable, then if $(P(A) \rightarrow A)$ is provable in $S$ then $A$ is provable in $S$. I understand the proof of this. 
I am interested in the question: 

Suppose $P(A) \rightarrow B$ and $P(B) \rightarrow A$ are provable in $S$. Does it then follow that $A$ and $B$ are both provable in $S$? 

Is this true? If so, why? 
I've tried proving it via variations on the proof of Lob's Theorem, and by trying to show that $P(A) \rightarrow A$ and $P(B) \rightarrow B$ are provable in $S$ given the assumptions, and thus that I can apply Lob's Theorem to get the conclusion. But I cannot seem to get anything to work.
 A: There's no need to dive into the proof - this can be directly reduced to a single application of Lob's theorem.
From $P(A)\rightarrow B$ and $P(B)\rightarrow A$, we get $P(A)\wedge P(B)\rightarrow A\wedge B$. But trivially we have $P(A)\wedge P(B)\leftrightarrow P(A\wedge B)$, so in fact from $P(A)\rightarrow B$ and $P(B)\rightarrow A$ we can conclude $$P(A\wedge B)\rightarrow A\wedge B.$$ Now apply Lob's theorem to $A\wedge B$.

In fact, even that's written more inefficiently than it needs to be - just observe that $P(A\wedge B)\rightarrow P(A)\wedge P(B)$ so under the hypotheses gives $B\wedge A$ - but the "backwards" way I've written it above might be more helpful in terms of seeing how we whipped it up: see how large a proposition we need to have a proof of in order to trigger every hypothesis, and then see if that lets us "catch our tail."
A: If the Hilbert-Bernays conditions hold and $P\to Q$ is provable, then $\Box P\to\Box Q$ is also provable.
Apply this to the proof of $\Box A \to B$ to get $\Box\Box A \to \Box B$, and combine this with $\Box B \to A$, to get $\Box \Box A \to A$.
Now repeat the usual proof of Löb's theorem with $\Box\Box$ instead of $\Box$ everywhere.
