 \(A(x_1 /t_1 , \ldots ,x_n /t_n)\) is the wff resulting from simultaneously replacing each \(x_i\) in \(A\) with \(t_i\) (for \(1 \le i \le n)\), provided \(t_i\) is free for \(x_i\) in \(A\)). For example, given this principle, [\(\lambda x (R(x) \amp S(x))](j)\) is the case iff \((R(j) \amp S(j))\) is also the case.