Understanding Symbolic Logic, Virginia Klenk, Prentice Hall, 2008, 5th edition, Unit 20, 1(l), p. 381

There are, I'm sure, other ways of coming to grips with the proof of this argument, exploiting perhaps some of the disjunctions, but the one below suggested itself to me first and here it is.

There are exactly three composers in the room. Exactly one of the composers in the room is a pianist. Any composer in the room who is not a pianist is an opera singer. Therefore, there are at least two opera singers in the room.

1. (∃x)(∃y)(∃z){Cx • Cy • Cz • Rx • Ry • Rz • ¬ (x = y) • ¬ (x = z) • ¬ (y = z) • (w)[(Cw • Rw) ⊃(w = x ∨ w = y ∨ w = z)]}
2. (∃x){Cx • Rx • (y)[(Cy • Ry) ⊃y = x] • Px}
3. (x)[(Cx • Rx • ¬ Px) ⊃Ox]
4. ∴(∃x)(∃y)[Ox • Oy • Rx • Ry • ¬ (x = y)]
5. * ¬ (∃x)(∃y)[Ox • Oy • Rx • Ry • ¬ (x = y)] ......... AIP
6. * (x)(y)[(Ox • Oy • Rx • Ry) ⊃ (x = y)] ......... 5 QC
7. * (∃y)(∃z){Ca • Cy • Cz • Ra • Ry • Rz • ¬ (a = y) • ¬ (a = z) • ¬ (y = z) • (w)[(Cw • Rw) ⊃(w = a ∨ w = y ∨ w = z)]} ......... 1 EI x/a
8. * (∃z){Ca • Cm • Cz • Ra • Rm • Rz • ¬ (a = m) • ¬ (a = z) • ¬ (m = z) • (w)[(Cw • Rw) ⊃(w = a ∨ w = m ∨ w = z)]} ......... 7 EI y/m
9. * Ca • Cm • Cr • Ra • Rm • Rr • ¬ (a = m) • ¬ (a = r) • ¬ (m = r) • (w)[(Cw • Rw) ⊃(w = a ∨ w = m ∨ w = r)] ......... 8 EI z/r
10. * ¬ (a = m) ......... 9 Simp.
11. * Ci • Ri • (y)[(Cy • Ry) ⊃y = i] • Pi ......... 2 EI x/i
12. * (y)[(Cy • Ry) ⊃y = i] ......... 11 Simp.
13. * (Cm • Rm) ⊃m = i ......... 12 UI y/m
14. * Cm • Rm ......... 9 Simp.
15. * m = i ......... 14,13 MP
16. * ¬ (a = i) ......... 15,10 Id
17. * (Ca • Ra) ⊃a = i ......... 12 UI y/a
18. * ¬ (Ca • Ra) ......... 16,17 MT
19. * ¬ Ca ∨¬ Ra ......... 18 DeM
20. * Ca ......... 9 Simp.
21. * ¬ Ra ......... 20,19 DS
22. * Ra ......... 9 Simp.
23. * Ra • ¬ Ra ......... 21,22 Conj.
24. ¬ ¬ (∃x)(∃y)[Ox • Oy • Rx • Ry • ¬ (x = y)] ......... 5-23 IP
25. (∃x)(∃y)[Ox • Oy • Rx • Ry • ¬ (x = y)] ......... 24 DN