# Predicate logic natural deduction - proving conditional without existential elimination

I'm working through Paul Tomassi's Logic (here), and I'm attempting to prove the following sequent (Exercise 6.3, Question 10, p. 286):

∀y[Gy → Hy] : ∃x[Gx] → ∃y[Hy]

The catch is that the book hasn't yet given a rule for eliminating the existential quantifier. The approach I've been trying is to assume ∃x[Gx] for conditional proof and try to prove ∃y[Hy] from it, but I don't know how to make any progress if I can't eliminate the quantifier from ∃x[Gx].

The proof system is a Lemmon-style natural deduction system, with the rules:

• Conjunction introduction and elimination
• Disjunction introduction and elimination
• Modus ponens, modus tollens, conditional proof
• Biconditional introduction and elimination
• Double negation introduction and elimination

And:

• Universal quantifier introduction and elimination
• Existential quantifier introduction

Tomassi says the proof can be done in 7 lines, although I'm aware that that's very dependent on the specifics of the proof system. Any help appreciated!