The most general form of substitution theorems speaks about arbitrary contexts:

1. Define what it means to have a substitution $\sigma : \Gamma \to \Delta$ from a context $\Gamma$ to a context $\Delta$ (it's a simultaneous substitution, and in case of type dependencies it has to do the right thing.

2. Prove that if $\Delta \vdash e : A$ then $\Gamma \vdash e\sigma : A\sigma$.

In such generality there is no reliance on exchange rules and it all works in dependent type theory as well. The case suggested by Max New in his answer is a special case.

The most general form of substitution theorems speaks about arbitrary contexts:

1. Define what it means to have a substitution $\sigma : \Gamma \to \Delta$ from a context $\Gamma$ to a context $\Delta$ (it's a simultaneous substitution giving a term $\Gamma \vdash e : A$ for every $y : A$ appearing in $\Delta$, and in case of type dependencies we have to do it recursively).

2. Prove that if $\Delta \vdash e : A$ then $\Gamma \vdash e\sigma : A\sigma$.

In such generality there is no reliance on exchange rules and it all works in dependent type theory as well. The case suggested by Max New in his answer is a special case.