What assumptions can be used to prove the equivalence of two subformulae? Let $\tau$, $\sigma$ and $\sigma'$ denote formulae in some language of interest, and suppose we wish to show that $$\tau \wedge \sigma \iff \tau \wedge \sigma'.$$
Then obviously, it suffices to show that $$\sigma \iff \sigma',$$
and furthermore, we can use $\tau$ in our proof of the above equivalence. In other words, it suffices to show that
$$\tau \implies (\sigma \iff \sigma')$$
which is a weaker statement.

Similarly, suppose we wish to show that 
$$\tau \vee \sigma \iff \tau \vee \sigma'.$$
Once again, it clearly suffices to show that $$\sigma \iff \sigma',$$
and this time, we can also use $\neg \tau$ to demonstrate the above equivalence. In other words, it suffices to demonstrate that 
$$\neg \tau \implies (\sigma \iff \sigma')$$
which is weaker.

My question is this.
Suppose we have a complicated formula $\phi$ of propositional logic, or even better, predicate logic. We want to replace a subformula $\sigma$ of $\phi$ with another formula $\sigma'$, such that the resulting formula $\phi'$ is equivalent to $\phi.$ Clearly, if we can show $\sigma \iff \sigma'$, then we can be sure that $\phi \iff \phi'$. My question is, what additional assumptions can we use in order to show $\sigma \iff \sigma'$ such that it is safe to conclude that $\phi \iff \phi'$?
 A: In some propositional logics (the following is NOT confined to classical propositional logic, it will hold also for Wajsberg 3-valued calculus, Wajsberg-Slupecki 3-valued calculus, and some other propositional calculi), you'll have CpCqp, CCpqCCqpEpq around somewhere.  I'll take them as axioms and illustrate how to demonstrate the equivalence of CCpqCCqrCpr and CCCpqpp.  I won't construct a table here to show that CCpqCCqrCpr and CCCpqpp can't get derived from each other under the rules of detachment and uniform substitution.  Using the style of Lukasiewicz, the notation 1 p/Cpq * C2-6 indicates substituting "p" with Cpq in wff 1.  It has the same form as C wff 2 wff 6, where wff 2 comes as the antecedent, and 6 as the consequent.  Consequently, we will then detach wff 6.
Axiom 1 CpCqp.
Axiom 2 CCpqCCqpEpq.
Axiom 3 CCpqCCqrCpr.
Axiom 4 CCCpqpp.
1 p/CCpqCCqrCpr, q/CCCpqpp * C3-5

5 C CCCpqpp CCpqCCqrCpr.
1 p/CCCpqpp, q/CCpqCCqrCpr * C4-6

6 C CCpqCCqrCpr CCCpqpp.
2 p/CCCpqpp, q/CCpqCCqrCpr * C5-7

7 C CCpqCCqrCpr CCCpqpp E CCCpqpp CCpqCCqrCpr.
7 * C6-8

8 E CCCpqpp CCpqCCqrCpr.
Thus, anytime we have the above 4 wffs as either theorems or axioms (more generally, I follow Lukasiewicz and call them "theses"), given the assumptions you've made in the original post (I've talked to someone who has questioned them before), we can replace CCpqCCqrCpr with CCCpqpp when it appears as a subformula of a formula.
I may as well add another example not in the axiom set here.
  3  p/CCpqp, q/p * C4-9

9 CCprCCCpqpr.
  3 q/Cqp * C1-10

10 CCCqprCpr.
  1 p/CCprCCCpqpr, q/CCCqprCpr * C1-11

11 C CCCqprCpr CCprCCCpqpr.
  1 p/CCCqprCpr, q/CCprCCCpqpr * C1-12

12 C CCprCCCpqpr CCCqprCpr.
  2 p/CCCqprCpr q/CCprCCCpqpr * C11-13

13 CC CCprCCCpqpr CCCqprCpr E CCCqprCpr CCprCCCpqpr.
  13 * C12-14

14 E CCCqprCpr CCprCCCpqpr.
