Conference proceedings article:

Maria Luisa Bonet and Samuel R. Buss.
"On the deduction rule and the number of proof lines."

In Proceedings of the Sixth Annual IEEE Symposium on Logic in Computer Science. (LICS'91).  IEEE Computer Society Press, 1991, pp. 286-297.

Subsequent journal papers that subsume this conference paper:

A general deduction Frege proof system provides at most quadratic speedup over Frege proof systems. A nested deduction Frege proof system provides at most a nearly linear speedup over Frege system where by nearly linear'' is meant the ratio of proof lengths is $O(\alpha(n))$ where $\alpha$ is the inverse Ackermann function. A nested deduction Frege system can linearly simulate the propositional sequent calculus and hence a Frege proof system can simulate the propositional sequent calculus with proof lengths bounded by $O(n\cdot\alpha(n))$.