A Concise Introduction to Logic, Patrick J. Hurley, Wadsworth, 2006, 9th ed,. 8.7, III, 9 p. 448

The highest mountain is in Tibet. Therefore, there is a mountain in Tibet that is higher than any mountain not in Tibet. (Mx: x is a mountain; Hxy: x is higher than y; Tx: x is in Tibet)

1.     (∃x){Mx • (y)[(My • y ≠ x) ⊃ Hxy] • Tx} ∴ (∃x){Mx • Tx • (y)[(My • ~ Ty) ⊃ Hxy]} 2.     ~ (∃x){Mx • Tx • (y)[(My • ~ Ty) ⊃ Hxy]} 3.     (x) ~ {Mx • Tx • (y)[(My • ~ Ty) ⊃ Hxy]} 4.     (x){~ (Mx • Tx) v ~ (y)[(My • ~ Ty) ⊃ Hxy]} 5.     Mm • (y)[(My • y ≠ m) ⊃ Hmy] • Tm 6.     Mm • Tm • (y)[(My • y ≠ m) ⊃ Hmy] 7.     Mm • Tm 8.     ~ (Mm • Tm) v ~ (y)[(My • ~ Ty) ⊃ Hmy] 9.     ~ (y)[(My • ~ Ty) ⊃ Hmy] 10. (∃y) ~ [(My • ~ Ty) ⊃ Hmy] 11. (∃y) ~ [~ (My • ~ Ty) v Hmy] 12. (∃y)[(My • ~ Ty) • ~ Hmy] 13. Mr • ~ Tr • ~ Hmr 14. Tm • Mm 15. Tm 16. ~ Tr • Mr • ~ Hmr 17. ~ Tr 18. Tm • ~ Tr 19. m ≠ r 20. (y)[(My • y ≠ m) ⊃ Hmy] • Mm • Tm 21. (y)[(My • y ≠ m) ⊃ Hmy] 22. (Mr • r ≠ m) ⊃ Hmr 23. ~ Hmr • ~ Tr • Mr 24. ~ Hmr 25. ~ (Mr • r ≠ m) 26. ~ Mr v r = m 27. Mr 28. r = m 29. m = r 30. m ≠ r • m = r 31. ~ ~ (∃x){Mx • Tx • (y)[(My • ~ Ty) ⊃ Hxy]} 32. (∃x){Mx • Tx • (y)[(My • ~ Ty) ⊃ Hxy]}

AIP 2 QC 3 DM 1 UI 5 Com 6 Simp 4 UI 7,8 DS 9 QC 10 Impl 11 DM 12 EI 7 Com 14 Simp 13 Com 16 Simp 15,17 Conj 18 Id 6 Com 20 Simp 21 UI 16 Com 23 Simp 22,24 MT 25 DM 13 Simp 26,27 DS 28 Id 28,29 Conj 2-30 IP 31 DN