Symbolic Logic, Irving M. Copi, Prentice Hall, 5th edition, 1979, ex. 2, p.132

The aim is to construct a formal proof of validity for the following argument. Hint: best not to mess around with a straight assumption for conditional proof, however promising it might look, because we are bound to fall foul of the principle whereby the instantiating variable, or the instantiating constant, must be free in at least all those places in the instantiating statement where the general variable is free in the 'decapitated' (with the quantifier removed) general statement. Thus, indirect proof, which produces an elegant deduction.

1. (x)[(∃y)Byx ⊃(z)Bxz]
2. ∴ (y)(z)(Byz ⊃Bzy)
3. * ¬ (y)(z)(Byz ⊃Bzy) / AIP
4. * (∃y)(∃z)(Byz • ¬ Bzy) / 3CQ
5. * (∃z)(Baz • ¬ Bza) / 4EI y/a
6. * Bam • ¬ Bma / 5EI z/m
7. * Bam / 6Simp.
8. * ¬ Bma / 6Simp.
9. * (∃y)Bym ⊃(z)Bmz / 1UG x/m
10. * (∃z) ¬ Bmz / 8EG
11. * ¬ (z)Bmz / 10CQ
12. * ¬ (∃y)Bym / 9,11MT
13. * (y) ¬ Bym / 12CQ
14. * ¬ Bam / 13UI y/a
15. * Bam • ¬ Bam / 7,14Conj.
16. ¬ ¬ (y)(z)(Byz ⊃Bzy) / 3-15IP
17. (y)(z)(Byz ⊃Bzy) / 16DN