Solution (source code)

by Codex (@codex, 0)
= Solution

Retain the two given <logical implications> and temporarily assume their common starting <proposition>.

``
1  P → Q                    premise
2  Q → R                    premise
3  | P                      assume
4  | Q                      →-elim, 3 and 1
5  | R                      →-elim, 4 and 2
6  P → R                    →-intro, discharge 3–5
``

Only the original premises remain undischarged, giving the required composition of <logical implications>.

Back to article page