Understanding Symbolic Logic, Virginia Klenk, Pearson Prentice Hall, 2008, Unit 18, Ex.1, problem (r), p. 354

We have to derive the conclusion from the premises given. Hint: It is tempting to use indirect proof because the conclusion is a simple existential statement, but this would not work very effectively here. It is easier to instantiate the premises and work through them until we isolate, by Modus Ponens, Wz on the first line.

1. (x){[Ax • ¬ (y)(Dxy ⊃Rxy)] ⊃(z)(Tzx ⊃Wz)}
2. ¬ (∃x)(∃y)(Tyx • ¬ Dxy)
3. ¬ (x)[Ax ⊃(y)(Tyx ⊃Rxy)
4. ∴(∃x)Wx
5. (∃x)[Ax • (∃y)(Tyx • ¬ Rxy) ......... 3CQ
6. (x)(y)(Tyx ⊃Dxy) ......... 2CQ
7. Aa • (∃y)(Tya • ¬ Ray) ......... 5EI x/a
8. Aa ......... 7Simp.
9. (∃y)(Tya • ¬ Ray) ......... 7Simp.
10. Tma • ¬ Ram ......... 9EI y/m
11. Tma ......... 10Simp.
12. ¬ Ram ......... 10Simp.
13. (y)(Tya ⊃Day) ......... 6UI x/a
14. Tma ⊃Dam ......... 13UI y/m
15. Dam ......... 11,14MP
16. Dam • ¬ Ram ......... 15,12Conj.
17. (∃y)(Day • ¬ Ray) ......... 16EG
18. (∃y)¬ ( ¬ Day ∨ Ray) ......... 17DeM
19. (∃y)¬ (Day ⊃ Ray) ......... 18MI
20. ¬ (y)(Day ⊃Ray) ......... 19CQ
21. [Aa • ¬ (y)(Day ⊃Ray)] ⊃(z)(Tza ⊃Wz)} ......... 1UI x/a
22. Aa • ¬ (y)(Day ⊃Ray) ......... 8,20Conj.
23. (z)(Tza ⊃Wz) ......... 22,21MP
24. Tma ⊃Wm ......... 23UI z/m
25. Wm ......... 11,24MP
26. (∃x)Wx ......... 25UG