Jacques Herbrand Proves the Deduction Theorem

In his doctoral thesis, Recherches sur la théorie de la démonstration, printed in Warsaw, Poland, in 1930 French mathematician Jacques Herbrand, a student at the École normale supérieure in Paris proved "the deduction theorem." 

 “The main product of Herbrand’s short life (he died in a skiing accident [at the age of 23]) was his thesis, in which he found two ways of proving that tautologies are provable. One was based upon a means of matching any quantified formula with a quantifier-free mate and proving that each was derivable; it reversed the handling of quantifications in Principia mathematica, *9, and also its systematic application in the second edition. The other method drew on model theory and normal forms, as developed by Leopold Löwenheim and Thoraf Skolem. A highlight was a result which became known as ‘the deduction theorem’; it took the form that if the premises of a theory were stated as a single conjunction H, then a proposition P was true within it if and only if ‘H ∩ P be a propositional identity’ . . . In effect though not in intention, he clarified some of Bertrand Russell’s conflations and implication and inference, and also removed a standard sloppiness among mathematicians when (not) relating a proof to its theorem. While several proofs were unclear and even defective, the thesis inspired important new lines of research” (Grattan-Guinness, The Search for Mathematical Roots 1870-1940 [2000] 550).

Van Heijenoort, From Frege to Gödel. A Source Book in Mathematical Logic (1967) 525-81.