Prove: $\varphi_1 =\!\mathrel|\mathrel|\!= \varphi_2 \implies \varphi_1[\psi/p] =\!\mathrel|\mathrel|\!= \varphi_2[\psi/p]$.
We've proven that $\varphi_1 =\!\mathrel|\mathrel|\!= \varphi_2 \implies \psi[\varphi_1/p] =\!\mathrel|\mathrel|\!= \psi[\varphi_2/p]$.
Maybe you could give me a hint what way of proving I should use? I don't see over wich formula or rank I could use induction in a useful way..
($\phi =\!\mathrel|\mathrel|\!= \psi$ means $\phi \models \psi$ and $\psi \models \phi$)
Let $\varphi_1 =\!\mathrel|\mathrel|\!= \varphi_2$.
Let $v$ be so that $|p|_v$ = 1. If now $|\psi|_v = 1$ then clearly $\varphi_1[\psi/p] =\!\mathrel|\mathrel|\!= \varphi_2[\psi/p]$ (is this clear?).
Accordingly: Let $v$ be so that $|p|_v$ = 0. If now $|\psi|_v = 0$ then clearly $\varphi_1[\psi/p] =\!\mathrel|\mathrel|\!= \varphi_2[\psi/p]$ (is this clear?).
I don't know how to approach the cases when $|p|_v$ = 0 while $|\psi|_v = 1$ and $|p|_v$ = 1 while $|\psi|_v = 0$.
Other attempt:
Show the equivalent statement $\quad |\!\!\!= \varphi_1 \leftrightarrow \varphi_2 \implies |\!\!\!= \varphi_1[\psi/p] \leftrightarrow \varphi_2[\psi/p] $
Notice, that $\quad \varphi_1[\psi/p] \leftrightarrow \varphi_2[\psi/p] \quad \equiv \quad (\varphi_1 \leftrightarrow \varphi_2)[\psi/p]$
Let now $|\!\!\!= \varphi_1 \leftrightarrow \varphi_2$. Then $\varphi_1 \leftrightarrow \varphi_2$ is a tautology and hence is true for any valuation $v$. In particular $\varphi_1 \leftrightarrow \varphi_2$ is true independent of whether $|p|=0$ or $|p|=1$. It follows (is this right?) that $(\varphi_1 \leftrightarrow \varphi_2)[\psi/p]$ is also true for any valuation $v$ as well. The claim follows.
What about this?