Symbolic Logic, Irving M. Copi, 5th edition, p. 150, problem 8

The argument is put thus:

Anyone who has climbed Mt Blanc is braver than anyone who has not. Of all those on our team, only the youngest has climbed Mr Blanc. Everyone on our team is a veteran. Therefore, the bravest member of our team is a veteran.

(Cx: has climbed Mt Blanc, Tx: is on our team, Vx: is a veteran, Bxy: is braver than y, Oxy: is older than y)

1. (x)[Cx ⊃(y)(¬ Cy ⊃Bxy)]
2. (∃x){Tx • (y){[Ty • ¬ (y = x)] ⊃(Oyx • ¬ Cx)} • Cx}
3. (x)(Tx ⊃Vx)
4. ∴ (∃x){Tx • (y){[Ty • ¬ (y = x)] ⊃Bxy} • Vx}
5. * ¬ (∃x){Tx • (y){[Ty • ¬ (y = x)] ⊃Bxy} • Vx} / AIP
6. * (x){{Tx • (y){[Ty • ¬ (y = x)] ⊃Bxy} ⊃¬ Vx} / 5QC
7. * Tm • (y){[Ty • ¬ (y = m)] ⊃(Oym • ¬ Cm)} • Cm / 2EI x/m
8. * Tm / 7Simp.
9. * Cm / 7Simp.
10. * Tm ⊃Vm / 3UI x/m
11. * Vm / 8,10MP
12. * {Tm • (y){[Ty • ¬ (y = m)] ⊃Bmy}} ⊃¬ Vm / 6UI x/m
13. * ¬ {Tm • (y){[Ty • ¬ (y = m)] ⊃Bmy}} / 11,12MT
14. * ¬ Tm ∨ ¬ (y){[Ty • ¬ (y = m) ⊃Bmy } / 13MI
15. * ¬ (y){[Ty • ¬ (y = m) ⊃Bmy } / 8,14DS
16. * (∃y)[Ty • ¬ (y = m) • ¬ Bmy) / 15QC
17. * Ta • ¬ (a = m) • ¬ Bma / 16EI y/a
18. * ¬ Bma / 17Simp.
19. * Cm ⊃(y)(¬ Cy ⊃Bmy) / 1UI x/m
20. * (y)(¬ Cy ⊃Bmy) / 9,19MP
21. * ¬ Ca ⊃Bma / 20UI y/a
22. * Ca / 18,21MT
23. * Ta • ¬ (a = m) / 17Simp.
24. * (y){[Ty • ¬ (y = m)] ⊃(Oym • ¬ Cm)} / 7Simp.
25. * [Ta • ¬ (a = m)] ⊃(Oam • ¬ Cm)} / 24UI y/a
26. * Oam • ¬ Cm / 23,25MP
27. * ¬ Cm / 26Simp.
28. * Cm • ¬ Cm / 22,27Conj.
29. ¬ ¬ (∃x){Tx • (y){[Ty • ¬ (y = x)] ⊃Bxy} • Vx} / 5-28IP
30. (∃x){Tx • (y){[Ty • ¬ (y = x)] ⊃Bxy} • Vx} / 29DN