Solution (source code)

= Solution

Let tuples $\bar a\in M\models T$ and $\bar b\in N\models T$ have the same quantifier-free type. The map $\bar a\mapsto\bar b$ extends to an isomorphism between the substructures they generate. Identify these substructures with one structure $A$. Both expanded models satisfy $T\cup D(A)$, which is complete by hypothesis, so they satisfy the same formulas with parameters from $A$. Thus $\bar a$ and $\bar b$ have the same complete type.

Therefore every isomorphism between substructures of models of $T$ is partial elementary. By compactness, this implies that every formula is equivalent modulo $T$ to a quantifier-free formula: otherwise two tuples with the same quantifier-free type but different truth values could be constructed. This is the <common-substructure test for quantifier elimination>, so $T$ admits <quantifier elimination>.