\begin{definition}[Definition:Derived Rule]
Let $\LL$ be a formal language.
Let $\mathscr P$ be a proof system for $\LL$.
A '''derived rule''' for $\mathscr P$ is a rule of inference $R$ such that:
:The proof system $\mathscr P'$, obtained by adding $R$ to $\mathscr P$, is equivalent to $\mathscr P$.
That is, $R$ is a '''derived rule''' {{iff}} it does not extend the collection of $\mathscr P$-theorems.
\end{definition}