Baaz, Matthias, and Richard Zach. 1994. “Short Proofs of Tautologies Using the Schema of Equivalence.” In Computer Science Logic. 7th Workshop, CSL ’93, Swansea. Selected Papers, edited by Egon Börger, Yuri Gurevich, and Karl Meinke, 33–35. LNCS 832. Berlin: Springer. DOI:10.1007/BFb0049322

It is shown how the schema of equivalence can be used to obtain short proofs of tautologies A, where the depth of proofs is linear in the number of variables in A.