I think the "soft" approach uses the soundness and completeness theorems.

The idea of the hard approach is that any parameter or a free variable can be systematically replaced throughout a derivation by something else, and the resulting formula sequence is be a valid derivation. That is, an n-ary predicate symbol P can be replaced by a formula

in the sense that every occurrence of

for some terms

is replaced by

. Similarly, a constant can be replaced by any term. The replacement has to be done in every formula of the derivation, including the axioms. So, for example, P can be replaced by the formula x = x (alternatively, by ~(x = x)) for a fresh variable x.

This works because such substitution converts axioms into axioms. Also, if in the original derivation Modus Ponens was aplied to A -> B and A, the substitution converts these formulas into some A' -> B' and A', so MP is again applicable. Formally, one proves that a derivation remains valid by induction on the length of the derivation.

This is just an outline; feel free to discuss the details.