Can biconditional statements that are not logically equivalent replace each other in bigger sentences?

Question

I've always wondered whether biconditional statements that are not logically equivalent validly replace each other in bigger sentences, on the basis that since they must have the same truth values therefore every sentence that they are in should have the same truth values.

It seems that with enough rules of inference in a proof, you can always end up with a "replacement": if I have $(P\iff Q)$ and a sentence $S_P$ with subsentence $P,$ then the sentence $S_Q$ with subsentence $Q$ can always be deduced.

Example

Let $(R\implies (\neg P\land S\implies T))$ be $S_P.$

Let $(R\implies (\neg Q\land S\implies T))$ be $S_Q.$

1. $P\iff Q$ Premise
2. $R\implies (\neg P\land S\implies T)$ Premise
3. $S_P\land (P\iff Q))\implies S_Q$ Logical Truth (Tautology)
4. $S_P\land (P\iff Q))$ Adjunction (2)(1)
5. $S_Q$ Modus Ponendo Ponens (3)(4)

It seems this would work no matter what $S_P$ is. But if this were the case, then why is "replacement" always limited to logically equivalent sentences?

I ask because there has been many proofs where it would have saved lots of time using a replacement from a biconditional, rather than deducing the replacement sentence step-by-step.

I've been told that two sentences are logical equivalent if and only if they have the same truth values in every model. So, while 1+1=2⟺99+1=100 is a true biconditional, assuming we are speaking about arithmetic, in a different model 1, 2, +, 99, and 100 could be defined differently, giving a different truth value to the sentence.

Answer 1

Your reasoning about replacement is correct! I think the answers you got on the linked question are a little misleading for your purposes. Logical equivalence in the strict sense used there depends on which rules/definitions/axioms you consider fixed and which ones you allow to vary when considering alternative models; the counterexamples given are based on models where symbols like + have been given nonstandard meanings (treating only the logic symbols as fixed since we want logical equivalence). These examples reflect the fairly obvious fact that if my "+" means something different from your "+", then your proof of a statement involving + is invalid to me (unless you proved something like $x=y\implies x+x=y+y$, using only the syntactic form of +).

When doing math in practice, we're only interested in models that satisfy our definitions and axioms (about the properties of sets, numbers, etc.), and when you prove $P\iff Q$ from those definitions and axioms, you are proving that $P$ and $Q$ have the same truth value in every such model. This justifies substituting one for the other in any expression. (The only models where the substitution fails are ones that reinterpret the symbols of your language in a way that violates your definitions/axioms, and the whole point of establishing and using definitions/axioms is to exclude those models from consideration.)