I have troubles showing the following (it's a slightly abridged version of Exercise 16.1 form Boolos and Jeffrey's Computability and Logic (3rd ed.)}):
$\textsf{Prv}(y)$ is a provability predicate for some consistent (first-order) theory $T$ (which is an extension of Robinson arithmetic) and $D(y)$ is the formula ($\textsf{Prv}(y) \ \& \ y \neq \ulcorner \textbf{0} = \textbf{1} \urcorner$).
Show that $D(y)$ meets [the third Hilbert-Bernays provability] condition: $\vdash_T D(\ulcorner A \urcorner)\rightarrow D(\ulcorner D(\ulcorner A \urcorner) \urcorner$).
My strategy was to derive separately:
(A) $\vdash_T (\textsf{Prv}(\ulcorner A \urcorner) \ \& \ \ulcorner A \urcorner \neq \ulcorner \textbf{0} = \textbf{1} \urcorner) \rightarrow \ulcorner (\textsf{Prv}(\ulcorner A \urcorner) \ \& \ \ulcorner A \urcorner \neq \ulcorner \textbf{0} = \textbf{1} \urcorner) \urcorner \neq \ulcorner \textbf{0} = \textbf{1} \urcorner$; and
(B) $\vdash_T (\textsf{Prv}(\ulcorner A \urcorner) \ \& \ \ulcorner A \urcorner \neq \ulcorner \textbf{0} = \textbf{1} \urcorner) \rightarrow \textsf{Prv}(\ulcorner (\textsf{Prv}(\ulcorner A \urcorner) \ \& \ \ulcorner A \urcorner \neq \ulcorner \textbf{0} = \textbf{1} \urcorner) \urcorner)$.
and combine two to get the result.
(A) seems like a straightforward theorem: if the consequent were false and antecedent true, $T$ would be inconsistent. But how can I get to (B)? I figured out that:
$\vdash_T (\textsf{Prv}(\ulcorner A \urcorner) \ \& \ \ulcorner A \urcorner \neq \ulcorner \textbf{0} = \textbf{1} \urcorner) \rightarrow [\textsf{Prv}(\ulcorner\textsf{Prv}(\ulcorner A \urcorner)\urcorner) \ \& \ \ulcorner A \urcorner \neq \ulcorner \textbf{0} = \textbf{1} \urcorner]$
But, then, can I get from $[\textsf{Prv}(\ulcorner\textsf{Prv}(\ulcorner A \urcorner)\urcorner) \ \& \ \ulcorner A \urcorner \neq \ulcorner \textbf{0} = \textbf{1} \urcorner]$ to $\textsf{Prv}(\ulcorner (\textsf{Prv}(\ulcorner A \urcorner) \ \& \ \ulcorner A \urcorner \neq \ulcorner \textbf{0} = \textbf{1} \urcorner) \urcorner)$ without much fuss? Does the former imply the latter?