Concerning the CP that takes place between lines 11-13. Is that a vilid use of CP? Am I allowed to assume -Q for RAA on line eleven, then Assume P for CP to prove (P -> -Q), then derive P -> -Q from 11,12 CP, despite the fact that -Q is assumed ( line 11) before we assume P for CP(line 12)?

Hope that makes sense. Thanks!

¬(P→¬Q) |- (P & Q)
1 1. ¬(P→¬Q) A
2 2. ¬P A (aim for contradiction and use RAA to get ¬¬P)
3 3. P A (aim for ¬Q and use CP to get (P→¬Q))
4. 4. Q A (aim for contradiction and use RAA to get ¬Q)
2,3 5. P&¬P 3,2 &I
2,3 6. ¬Q 4,5 RAA
2 7. P→¬Q 3,6 CP
1,2 8. (P→¬Q)&¬(P→¬Q) 7,1 &I
1 9. ¬¬P 2,8 RAA
1 10. P 9 DN
11 11. ¬Q A (aim for contradiction and use RAA to get ¬¬Q)
12 12. P A (use CP to get (P→¬Q))
11 13. (P → ¬Q) 12,11 CP
1,11 14. (P→¬Q)&¬(P→¬Q) 13,1 &I
1 15. ¬¬Q 11,14 RAA
1 16. Q 15 DN
1 17. P&Q 10,16 &I