Symbolic Logic, Irving M. Copi, Prentice Hall, 1979, 5th edition, p. 150, problem 10

We are asked to prove the validity of the following argument, where Ax - x was an accompanist, Bx - x was a bagpiper, and Cx - x was in the cabin. The argument goes:

All accompanists were bagpipers. All bagpipers were in the cabin. At most two individuals were in the cabin. There were at least two accompanists. Therefore, there were exactly two bagpipers.

1. (x)(Ax ⊃Bx)
2. (x)(Bx ⊃ Cx)
3. (x)(y)(z)[(Cx • Cy • Cz) ⊃(x = y ∨x = z ∨ y = z)]
4. (∃x)(∃y)[Ax • Ay • ¬ (x = y)]
5. ∴(∃x)(∃y){Bx • By • ¬ (x = y) • (z)[Bz ⊃(z = x ∨z = y)]}
6. * ¬ (∃x)(∃y){Bx • By • ¬ (x = y) • (z)[Bz ⊃(z = x ∨z = y)]} ......... AIP
7. * (x)(y){[Bx • By • ¬ (x = y)] ⊃(∃z)[Bz • ¬ (z = x) • ¬ (z = y)]} ......... 6CQ
8. * (∃y)[Aa • Ay • ¬ (a = y)] ......... 4EI x/a
9. * Aa • Am • ¬ (a = m) ......... 8EI y/m
10. * Aa ⊃ Ba ......... 1UI x/a
11. * Aa ......... 9Simp.
12. * Ba ......... 11,10MP
13. * Am ⊃ Bm ......... 1UI x/m
14. * Am ......... 9Simp.
15. * Bm ......... 14,13MP
16. * ¬ (a = m) ......... 9Simp.
17. * Ba • Bm • ¬ (a = m) ......... 12,15,16Conj.
18. * (y){[Ba • By • ¬ (a = y)] ⊃(∃z)[Bz • ¬ (z = a) • ¬ (z = y)]} ......... 7UI x/a
19. * [Ba • Bm • ¬ (a = m)] ⊃(∃z)[Bz • ¬ (z = a) • ¬ (z = m)] ......... 18UI y/m
20. * (∃z)[Bz • ¬ (z = a) • ¬ (z = m)] ......... 17,19MP
21. * Bh • ¬ (h = a) • ¬ (h = m) ......... 20EI z/h
22. * Bh ⊃Ch ......... 2UI x/h
23. * Bh ......... 21Simp.
24. * Ch ......... 22,23MP
25. * Ba ⊃Ca ......... 2UI x/a
26. * Ca ......... 12,25MP
27. * Bm ⊃Cm ......... 2UI x/m
28. * Cm ......... 14,27MP
29. * Ca • Cm • Ch ......... 26,24,28Conj.
30. * (y)(z)[(Ca • Cy • Cz) ⊃(a = y ∨a = z ∨ y = z)] ......... 3UI x/a
31. * (z)[(Ca • Cm • Cz) ⊃(a = m ∨a = z ∨ m = z)] ......... 30UI y/m
32. * (Ca • Cm • Ch) ⊃(a = m ∨a = h ∨ m = h) ......... 31UI z/h
33. * a = m ∨a = h ∨ m = h ......... 29,32MP
34. * a = h ∨ m = h ......... 16,33DS
35. * ¬ (h = a) ......... 21Simp.
36. * m = h ......... 35,34DS
37. * ¬ (h = m) ......... 21Simp.
38. * h = m ......... 36Comm.
39. * h = m • ¬ (h = m) ......... 37,38Conj.
40. ¬ ¬ (∃x)(∃y){Bx • By • ¬ (x = y) • (z)[Bz ⊃(z = x ∨z = y)]} ......... 6-39IP
41. (∃x)(∃y){Bx • By • ¬ (x = y) • (z)[Bz ⊃(z = x ∨z = y)]} ......... 40DN