= Solution
For <implication creation rule>, keep $\psi$ available and discharge an otherwise unused antecedent:
``
1 ψ given
2 | φ assume
3 | ψ available from 1
4 φ → ψ →-intro, discharge 2–3
``
For <implication distribution rule>, write $H=\phi\to(\psi\to\rho)$. The <logical derivation> below keeps $H$ available and discharges exactly the two <temporary assumptions>:
``
1 φ → (ψ → ρ) given
2 | φ → ψ assume
3 | | φ assume
4 | | ψ →-elim, 3 and 2
5 | | ψ → ρ →-elim, 3 and 1
6 | | ρ →-elim, 4 and 5
7 | φ → ρ →-intro, discharge 3–6
8 (φ → ψ) → (φ → ρ) →-intro, discharge 2–7
``
These justify both <derived inference rules> using Figure 2 primitives. Their rule forms retain any other surrounding assumptions; they are not unconditionally asserted conclusions after the displayed numerator is forgotten.
Back to article page
