= Solution
The existential premise is $\exists x\,(Q(x)\to R(x))$, with the <logical implication> inside the <existential quantifier>. Eliminate it using a fresh witness $a$, specialize $\forall x\,Q(x)$ to that same witness, and introduce the required <existential quantifier> before closing the witness subproof:
|| Line
|| Context
|| Formula
|| Justification
| 1
| $\{1\}$
| $\exists x\,(Q(x)\to R(x))$
| Premise
| 2
| $\{1,2\}$
| $\forall x\,Q(x)$
| Premise
| 3
| $\{1,2,3\}$
| $Q(a)\to R(a)$
| Temporary assumption
| 4
| $\{1,2,3\}$
| $Q(a)$
| <universal elimination> $\forall\text{-elim}$ on 2; instantiate at $a$
| 5
| $\{1,2,3\}$
| $R(a)$
| <implication elimination rule> $\to\text{-elim}$ on 3, 4
| 6
| $\{1,2,3\}$
| $\exists x\,R(x)$
| <existential quantifier introduction rule> $\exists\text{-intro}$ on 5; witness $a$
| 7
| $\{1,2\}$
| $\exists x\,R(x)$
| <existential quantifier elimination rule> $\exists\text{-elim}$ on 1, 6; discharge 3; $a$ fresh
The <eigenvariable> $a$ is absent from the premises and from $\exists x\,R(x)$. Consequently,
$$
\boxed{\exists x\,(Q(x)\to R(x)),\ \forall x\,Q(x)\vdash\exists x\,R(x).}
$$
Back to article page
