Edit: The S combinator is not exactly Hypothetical Syllogism, which is also known as double implication elimination, but may be used to derive each other with simplification and implication elimination: https://en.wikipedia.org/wiki/Hypothetical_syllogism#Alterna... and the K combinator is simplification and not Peirce's Law: https://en.wikipedia.org/wiki/Hilbert_system#Further_connect... Also, the first exact instance of S is likely P3 in Frege's propositional calculus.