The textbook's way of deriving a natural deduction proof of $\vdash((\phi\leftrightarrow\psi)\leftrightarrow\phi)$ feels wrong.

Question

The problem is

"Show that if we have a derivation $D$ of $\psi$ with no undischarged assumptions, then we can use it to construct, for any statement $\phi$, a derivation of $((\phi\leftrightarrow\psi)\leftrightarrow\phi)$ with no undischarged assumptions."

Here is my solution.

Below is the textbook's solution.

As you can see on the textbook solution, $\phi$ and $\psi$ cross over to another branch to introduce $\rightarrow$. The textbook didn't mention it was possible. Is the textbook solution a correct derivation of the proof?

Update 1 : I want to solve exercises with what the author explicitly allowed in the textbook. The author wrote:

Answer 1

There is no error; an allowed way to use $\to$-intro is to discharge a "non-existent" assumption, i.e.:

$\psi \vdash \phi \to \psi$,

as in the two top-right branches.

This corresponds to the fact that $\psi \to (\phi \to \psi)$ is a tautology; thus, assuming $\psi$, by modus ponens $(\phi \to \psi)$ follows, for $\phi$ whatever.

See the textbbok's comment on the rule, page 17:

The rule is still correctly applied if we do not discharge all of them; in fact the rule is correctly applied even if $\phi$ is not an assumption of $D$ at all, so that there is nothing to discharge. Example 2.4.4 (page 19) will illustrate these points.

Answer 2

There's no crossing over.   On one branch $\psi$ is true from the derivation (D).   On the other branch, $\phi$ is assumed, then later discharged.

It is just making use of an unusual form of conditional introduction; if something is true, then anything will imply it is true.   $p\vdash (q\to p)$

Where as the usual form is the deduction theorem: $(p\vdash q)\vdash p\to q$

$$\begin{array}{l|l:l} 1 & \psi & D\vdash \psi \\ 2 & \phi\to \psi & 1, {\to}\mathsf I \\ \hdashline 3 & \quad \phi & \textsf{Assume }\phi \\ 4 & \quad \psi\to \phi & 3,{\to}\mathsf I \\ 5 & \quad \phi\leftrightarrow \psi & 2, 4, {\leftrightarrow}\mathsf I \\ \hline 6 & \phi \to (\phi\leftrightarrow \psi) & 5, {\to}\mathsf I~ (\textsf{DT Discharges Assumption of }\phi) \end{array}$$

$$\require{enclose}\require{cancel}\enclose{circle}{A}\dfrac{\dfrac{\dfrac{\dfrac{D}{\psi}}{\phi\to\psi}{{\to}\mathsf I}\quad\dfrac{\cancel[color=red]{\color{blue}\phi}^{\enclose{circle}A}}{\psi\to\phi}{{\to}\mathsf I}}{\phi\leftrightarrow\psi}{{\leftrightarrow}\mathsf I}}{\color{blue}\phi\to(\phi\leftrightarrow\psi)}{{\to}\textsf{I (DT)}}$$