S. Cook and R. Reckhow earlier defined a propositional formulation of the pigeonhole principle [ibid. 44, 36-50 (1979; Zbl 0408.03044)]. This paper shows that there are polynomial size Frege proofs of this propositional pigeonhole principle. (A Frege proof is a propositional proof with modus ponens as its only rule; the size of a proof is the number of symbols in the proof.) This together with a theorem of A. Haken [Theor. Comput. Sci. 39, 297-308 (1985; Zbl 0586.03010)] gives another proof of A. Urquhart’s result [J. Assoc. Comput. Mach. 34, 209-219 (1987)] that Frege systems have an exponential speedup over resolution. This paper also discusses connections to provability in theories of bounded arithmetic.