Frege's theorem in propositional logic

Statement

In propositional logic, Frege's theorem refers to this tautology:

$$\big(P\to(Q\to R)\big)\to\big((P\to Q)\to(P\to R)\big)$$

The theorem already holds in one of the weakest logics imaginable, the constructive implicational calculus. The proof under the Brouwer–Heyting–Kolmogorov interpretation reads $f \mapsto g\mapsto p\mapsto (f(p)\circ g)(p)$. In words: "Let f denote a reason that P implies that Q implies R. And let g denote a reason that P implies Q. Then given a f, then given a g, then given a reason p for P, we know both that Q holds by g and that Q implies R holds by f. So R holds."

The truth table to the right gives a semantic proof. For all possible assignments of false () or true () to P, Q, and R (columns 1, 3, 5), each subformula is evaluated according to the rules for material conditional, the result being shown below its main operator. Column 6 shows that the whole formula evaluates to true in every case, i.e. that it is a tautology. In fact, its antecedent (column 2) and its consequent (column 10) are even equivalent.