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

We are to prove a tautology. Note that we can generalize by UG on line 18 to (x)Fx because we are now outside the scope of the assumption made on line 14.

├ ¬ (∃x)[Fx • (Ga ⊃Ha)] ≡ [(¬ Ga ∨Ha) ⊃ ¬ (∃x)Fx]

1. ¬ (∃x)[Fx • (Ga ⊃Ha)] ⊃[(¬ Ga ∨Ha) ⊃ ¬ (∃x)Fx]
2. * ¬ (∃x)[Fx • (Ga ⊃Ha)] / ACP
3. * (x)[Fx ⊃¬ (Ga ⊃Ha)] / 2QC
4. * * (∃x)Fx / ACP
5. * * Fm / 4EI x/m
6. * * Fm ⊃¬ (Ga ⊃Ha) / 3UI x/m
7. * * ¬ (Ga ⊃Ha) / 5,6MP
8. * (∃x)Fx ⊃¬ (Ga ⊃Ha) / 4-7CP
9. * (Ga ⊃Ha) ⊃¬ (∃x)Fx / 8Contrap.
10. * (¬ Ga ∨Ha) ⊃ ¬ (∃x)Fx / 9MI
11. ¬ (∃x)[Fx • (Ga ⊃Ha)] ⊃[(¬ Ga ∨Ha) ⊃ ¬ (∃x)Fx] / 2-10CP
12. [(¬ Ga ∨Ha) ⊃ ¬ (∃x)Fx] ⊃¬ (∃x)[Fx • (Ga ⊃Ha)]
13. * (¬ Ga ∨Ha) ⊃ ¬ (∃x)Fx / ACP
14. * * Fx / ACP
15. * * (∃x)Fx / 14EG
16. * * ¬ (¬ Ga ∨Ha) / 15,13MT
17. * Fx ⊃¬ (¬ Ga ∨Ha) / 14-16CP
18. * (x)[Fx ⊃¬ (¬ Ga ∨Ha)] / 17UG
19. * (x)[¬ Fx ∨¬ (¬ Ga ∨Ha)] / 18MI
20. * (x) ¬ [Fx • (Ga ⊃Ha)] / 19DeM
21. * ¬ (∃x)[Fx • (Ga ⊃Ha)] / 20QC
22. [(¬ Ga ∨Ha) ⊃ ¬ (∃x)Fx] ⊃¬ (∃x)[Fx • (Ga ⊃Ha)] / 13-21CP
23. {¬ (∃x)[Fx • (Ga ⊃Ha)] ⊃[(¬ Ga ∨Ha) ⊃ ¬ (∃x)Fx]} • {[(¬ Ga ∨Ha) ⊃ ¬ (∃x)Fx] ⊃¬ (∃x)[Fx • (Ga ⊃Ha)]} / 11,22Conj.
24. ¬ (∃x)[Fx • (Ga ⊃Ha)] ≡ [(¬ Ga ∨Ha) ⊃ ¬ (∃x)Fx] / 23BE