The converse of DT has powerful implications: it can be used to convert an axiom into an inference rule. For example, the axiom AND-1,

\vdash \phi \wedge \chi \rightarrow \phi

can be transformed by means of the converse of the deduction theorem into the inference rule

\phi \wedge \chi \vdash \phi

which is conjunction elimination, one of the ten inference rules used in the first version (in this article) of the propositional calculus.

— Wikipedia on Propositional calculus

2013.11.08 Friday ACHK