Subformula replacement theorem

Replacing one designated subformula occurrence in a propositional formula by another propositional formula preserves well-formedness. Induct on the context surrounding the occurrence: at the root the result is the replacement formula; under a connective apply the induction hypothesis to the affected child and rebuild the parent using its formation rule.

Replacing a designated subformula by a logically equivalent formula preserves logical equivalence of the surrounding propositional formulas. For any Boolean valuation the two expressions at the replaced node have the same truth value. Each logical connective preserves this agreement when its other inputs are unchanged. Induction from that node to the root proves agreement of the whole formulas under every valuation.