# My favourite proof

**3 February 2023**

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

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