1. In propositional logic, a formula $\phi \left[\psi /p\right]$ generated from formula $\phi$ by replacing every occurrence of the atomic formula $p$ with the formula $\psi$.

2. A rule of inference in propositional logic that for any atom $p$ and formula $\psi$, whenever a sentence $\phi$ is a theorem of a deductive system, one may infer that $\phi \left[\psi /p\right]$ is also a theorem of the system.