Propositional variable elimination ($A\equiv (A[p:=\top ]\wedge p)\vee (A[p:=\perp ]\wedge \neg p)$)

The displayed identity follows by testing the two possible truth values of $p$. Existentially forgetting $p$ gives $A[p:=\top ]\vee A[p:=\perp ]$. Repeating this operation produces a propositional formula on a specified remaining vocabulary. Logical truth constants are needed if that vocabulary is empty.

If $A⊢B$, eliminate the letters private to $A$ byEvery assignment satisfying $A$ satisfies one disjunct of $C$. If an assignment satisfies $C$, change only the eliminated letters to its witnessing assignment. The modified assignment satisfies $A$ and hence $B$, whose letters were unchanged. Thus $A\models C\models B$, and the propositional completeness theorem gives the two derivations. The interpolant uses only common letters; an empty common vocabulary is handled by logical truth constants.