My favourite proof

The Hypothetical syllogism states that from \(b \rightarrow c\) and \(a \rightarrow b\), we can deduce \(a \rightarrow c\)

Alternatively, this is \((b \rightarrow c \land a \rightarrow b) \rightarrow a \rightarrow c\)

In words this represents “if a implies b, and b implies c, then a implies c”. In sequent calculus the proof is as follows

1. (b -> c, a -> b)
2. b -> c            (conjunction-elimination-1, 1)
3. a -> b            (conjunction-elimination-2, 1)
 | 4. a              (assumption)
 | 5. b              (modus-ponens, 3, 4)
 | 6. c              (modus-ponens, 2, 5)
7. a -> c            (implication-introduction, 4 to 6)

In Haskell, the proof is much shorter

ghci> proof = uncurry (.)
ghci> :t proof
proof :: (b -> c, a -> b) -> a -> c

1. Curry-Howard Correspondence