A formal proof in propositional logic is considered a sequence of formulas such that every formula is either an axiom, a member of the presupposed set, or derived by previous ones through a rule of inference. If a formal system proves an equivalence $\phi\leftrightarrow\psi$, I.e. $\vdash\phi\leftrightarrow\psi$, can all occurrences of $\phi$ may be replaced in the proof by $\psi$ and vice versa?
If one haves a translation $t$ one logic $\vdash_1$ into another $\vdash_2$ s.t. the one proves $\vdash_2\phi\leftrightarrow t(\phi)$, does this then infer that $\Gamma\vdash_2\phi$ if and only if $t(\Gamma)\vdash_1t(\phi)$ by a translation of the elements of the proof.
Your second paragraph (even with your comment) is unclear, and, with your comment, seems require introducing a bunch of machinery and noise that has no bearing on the content of your question.
As for your first question, in classical propositional logic you can define a relation on formulas via $\varphi\sim\psi$ if and only if $\vdash\varphi\leftrightarrow\psi$. This relation is a congruence on formulas with respect to the logical connectives. That is, it's an equivalence relation (reflexive, symmetric, and transitive) and, if we define all other connectives in terms of $\neg$ and $\land$, that if $\varphi\sim\varphi'$ and $\psi\sim\psi'$ then $\neg\varphi\sim\neg\varphi'$ and $\varphi\land\psi\sim\varphi'\land\psi'$. Prove all of this.
You can then easily prove from modus ponens (do this), that if $\varphi\sim\psi$ then $\vdash\varphi$ if and only if $\vdash\psi$. Because $\sim$ is a congruence this means that for any formula containing $\varphi$, call it $F(\varphi)$, if $\varphi\sim\psi$ then $F(\varphi)\sim F(\psi)$, thus $\vdash F(\varphi)$ if and only if $\vdash F(\psi)$. You can use the deduction theorem to extend this to conditional provability.
As an addendum, if we quotient the set of formulas by $\sim$ we get the Lindenbaum-Tarski algebra which for classical propositional logic will be a Boolean algebra.