We are given a proof system with rules
- Modus Ponens $p \to q, p \vdash q$
- Right implication introduction $q\to p \to q$
- Distributive implication introduction $p \to (q \to r) \to (p \to q) \to (p \to r)$
We need to convert a given valid proof of $(x \land y) \vdash (y \land x)$ to a proof of $\vdash (x \land y \to y \land x)$ with rules above and from the original proof (below) (the Deduction Theorem is not allowed)
- $x \land y$
- $x \land y \to y$ (conjuction elimination)
- $y$
- $x \land y \to x$ (conjuction elimination)
- $x$
- $ y \to x \to y \land x$ (conjuction introduction)
- $ x \to y \land x $ (Modus Ponens)
- $ y \land x $ (Modus Ponens again)