I'm currently studying John Nolt's Outline of Logic ( Schaum's series).
According to the author, one can use natural deduction to prove some rules of natural deduction itself, for example the absorption rule ( chap. 4, Solved problem 4.33).
Example. Consider the following proof
(1) P --> Q hypothesis ( For conditional proof)
(2) ~ P v Q DF -->
(3) Q v ~ P Commut. v
(4) ~ ~ Q v ~ P DN
(5) ~ Q --> ~ P Df -->
(6) (P --> Q) --> ( ~Q --> ~P) Cond. Proof (1 - 5)
What did I prove here : a "rule" ? or simply the "sentence" :
(P--> Q) --> ( ~Q --> ~P)
Natural Deduction consists of a set of fundamental rules, which are each independent, and justified by the semantics of the connectives. The fundamental rules can be used to prove sentences which may be used to justify derived rules. Sometimes these sentences may be called Tautological Consequences (TautCon).
Here is the Natural Deduction proof for $\vdash (p\to q)\to(\lnot q\to\lnot p)$ using only the usual fundamental rules. (Note: in most Natural Deduction systems, implication equivalence is not actually considered a fundamental rule.)
$$\def\fitch#1#2{\quad\begin{array}{|l} #1 \\ \hline #2 \end{array}} \fitch{} {\fitch{1.~p\to q\hspace{14.75ex}\text{Assumption}} {\fitch{2.~\lnot q\hspace{14.5ex}\text{Assumption}} {\fitch{3.~p\hspace{12.5ex}\text{Assumption}} {4.~q\hspace{12.5ex}\text{1,3,Conditional Elimination} \\5.~\bot\hspace{11.75ex}\text{2,4,Negation Elimination}} \\6.~\lnot p\hspace{14.25ex}3{-}5,\text{Negation Introduction}} \\7.~\lnot q\to\lnot p\hspace{11.5ex}2{-}6,\text{Conditional Introduction}} \\8.~(p\to q)\to(\lnot q\to\lnot p)\hspace{2ex}1{-}7,\text{Conditional Introduction}}$$
Now, because this sentence is provable, we don't need to repeat all the above typesetting to apply conditional elimination. We can just cite such a proof to justify deriving $(\lnot \psi\to\lnot \phi)$ from $(\phi\to\psi)$. We can call doing this applying a derived rule of inference and, in this case, name it Contraposition .