Is is true that a logically equivalent proposition can be substituted in any deducible formula and still be deducible?

Question

If we have an axiom set $\mathcal A$ which contains all logic axioms, and $S,T$ are two formulas and $\mathcal A\vdash \{S \leftrightarrow T\}$. For a formula $P$ that $S$ is a sub-string of $P$, let $P[S:T]$ be the formula that we replace the sub-string $S$ in $P$ with $T$. Then my question is, is it true that $\mathcal A \vdash \{P \leftrightarrow P[S:T]\}$?

My idea is we can perform an induction on $\mathrm{len}(P) - \mathrm{len}(S)$, where $\mathrm{len}(P)$ is the length of the string $P$.

If $\mathrm{len}(P) - \mathrm{len}(S) = 0$, then $P = S$, and the conclusion is obviously true. If $\mathrm{len}(P) - \mathrm{len}(S) = n > 0$, the induction hypothesis says for any string $Q$ whose length is less than $P$ and $S$ is a sub-string of $Q$, we have $\mathcal A \vdash Q \leftrightarrow Q[S:T]$. Then, consider all three possibilities of the the first logic symbol in $P$:

• If $P = \lnot Q$, then we can use tautology $(Q \leftrightarrow Q[S:T]) \to (\lnot Q \leftrightarrow \lnot Q[S:T])$ to get the conclusion.

• If $P = Q \to R$, then $S$ is a substring of $Q$ or $R$, then we can use the tautolofies $$(Q \leftrightarrow Q[S:T]) \to ((Q \to R) \leftrightarrow (Q[S:T] \to R))$$and $$(R \leftrightarrow R[S:T]) \to ((Q \to R) \leftrightarrow (Q \to R[S:T]))$$to prove the conclusion.

• If $P = \forall x (Q)$, then we basically need to prove $\forall x (Q) \leftrightarrow \forall x(Q[S:T])$ from $Q \leftrightarrow Q[S:T]$. Let $Q[S:T] = W$, then we can use the following deduction:

  1. $ \forall x (W) \to W$ (Quantifier Axiom)
  2. $ W \to Q$ (Hypothethis)
  3. $ (\forall x (W) \to W) \to \big[(W \to Q) \to (\forall x (W) \to Q)\big]$ (Tautology)
  4. $ (W \to Q) \to (\forall x W \to Q)$ (MP, from 3 and 1)
  5. $ \forall x W \to Q$ (MP, from 4 and 2)
  6. $ \forall x\left[\forall x W \to Q\right]$ (Gen, from 5)
  7. $\big( \forall x \left[\forall x W \to Q\right]\big) \to (\forall x W \to \forall x Q)$ (Quantifier Axiom)
  8. $ \forall x W \to \forall x Q$ (MP, from 7 and 6)

  This proves one side, and using a similar deduction can prove the other side.

  Notice we used two quantifier axioms $\forall x(A) \to A$ and $\forall x(B \to A) \to (B\to \forall x(A))$ if $x$ does not occur freely in $B$. (I'm not sure what are their names....)

I wonder if there is any error in this proof?