Symbolic Logic, Dale Jacquette, Wadsworth, 2001, Chpt. 8, Ex. III, problem 16, p. 434

The task: give a natural deduction proof for the following tautology, ├ (x)(Fx ⊃Gx) ⊃(y)[(∃z)(Fz • Hyz) ⊃(∃z)(Gz • Hyz)].

├ (x)(Fx ⊃Gx) ⊃(y)[(∃z)(Fz • Hyz) ⊃(∃z)(Gz • Hyz)]

1. * (x)(Fx ⊃Gx) ......... ACP
2. * * (∃z)(Fz • Hyz) ......... ACP
3. * * Fa • Hya ......... 2EI z/a
4. * * Fa ⊃Ga ......... 1UI x/a
5. * * Fa ......... 3Simp.
6. * * Ga ......... 5,4MP
7. * * Hya ......... 3Simp.
8. * * Ga • Hya ......... 6,7Conj.
9. * * (∃z)(Gz • Hyz)] ......... 8EG
10. * (∃z)(Fz • Hyz) ⊃(∃z)(Gz • Hyz) ......... 2-9CP
11. (x)(Fx ⊃Gx) ⊃(y)[(∃z)(Fz • Hyz) ⊃(∃z)(Gz • Hyz)] ......... 1-10CP