Journal article:

Maria Luisa Bonet and Samuel R. Buss.
"The deduction rule and linear and near-linear proof simulations."
Journal of Symbolic Logic 58 (1993) 688-709.

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, the tree-like general deduction Frege calculus, and the natural deduction calculus. Hence a Frege proof system can simulate all those proof systems with proof lengths bounded by $O(n\cdot\alpha(n))$. Also we show that a Frege proof of $n$ lines can be transformed into a tree-like Frege proof of $O(n\log n)$ lines and of height $O(\log n)$. As a corollary of this fact we can prove that natural deduction and sequent calculus tree-like systems simulate Frege systems with proof lengths bounded by $O(n\log n)$.