 Subformula replacement

Subformula replacement is the operation of replacing one specified subformula occurrence by another logical formula. Its preservation of well-formedness is the subformula replacement theorem.