Proving Sequent using Natural Deduction RTP: $P \to Q, R \to \neg Q, (S\to \neg P)\to R \vdash (\neg T ∨ P)\to(T \to S)$ using primitive rules of natural deduction. I've attempted this question multiple times but keep getting stuck on trying to get $S$ so I can use a couple arrow introductions to get the conclusion.
Attempt:
1 (1) $P \to Q$ Assumption
2 (2) $R \to \neg Q$ Assumption
3 (3) $(S\to \neg P)\to R$ Assumption
4 (4) $(\neg T ∨ P)$ Assumption
5 (5) $T$ Assumption
4,5 (6) $P$ $4,5∨$E
1,4,5 (7) $Q$ $1,6\to$E
8 (8) $S$ Assumption
9 (9) $S\to \neg P$ Assumption
8,9 (10) $\neg P$ Assumption
4,5,9 (11) $\neg T$ 6,10RAA(8)
12 (12) R Assumption
2,12 (13) $\neg Q$ $2,12\to$E
1,2,4,5 (14) $~R$ 7,13RAA(12)
I realise now that I've eliminated almost all the necessary assumptions with only line 9 left over (those at lines 4 and 5 which will be eliminated via arrow introduction for the conclusion once I have $S$), but I don't know how I can proceed from here. Any help would be greatly appreciated.
 A: Here is a proof using "primitive rules" of Natural Deduction.
From line (4) $(¬T ∨ P)$ --- Assumption, we apply $(\lor \text E)$ with two sub-proofs:
The first one is straightforward:


*$\lnot T$ --- assumed [a] for $(\lor \text E)$


*$T$ -assumed [b]


*$\bot$ --- from 5) and 6) using $(\lnot \text E)$


*$S$ --- from 7) using $(\bot \text E)$



*$(T \to S)$ --- from 6) and 8) by $(\to \text I)$, discharging [b].


The second sub-proof:


*$P$ --- assumed [d] for $(\lor \text E)$


*$Q$ --- from 10) and 1) by $(\to \text E)$


*$R$ --- assumed [e]


*$\lnot Q$ --- from 12) and 2) by $(\to \text E)$


*$\bot$ --- from 11) and 13) by $(\lnot \text E)$


*$\lnot R$ --- from 12) by $(\lnot \text I)$, discharging [e]


*$(S \to \lnot P)$ --- assumed [f]


*$R$ --- from 16) and 3) by $(\to \text E)$


*$\bot$ --- from 15) and 17) by $(\lnot \text E)$


*$\lnot (S \to \lnot P)$ --- from 16) and 18) by $(\lnot \text I)$, discharging [f]


*$\lnot S$ --- assumed [g]


*$S$ --- assumed [h]


*$\bot$ --- from 20) and 21) by $(\lnot \text E)$


*$\lnot P$ --- from 22) by $(\bot \text E)$


*$(S \to \lnot P)$ --- from 21) and 23) by $(\to \text I)$, discharging [h]


*$\bot$ --- from 19) and 24) by $(\lnot \text E)$


*$S$ --- from 20) and 25) by $(\neg \neg \text E)$: if $\Gamma , \neg \varphi \vdash \bot$, then $\Gamma \vdash \varphi$, discharging [g]


*$(T \to S)$ --- from 26) by $(\to \text I)$.
Now we have derived $(T \to S)$ in the two sub-proofs and we can close the $(\lor \text E)$:


*$(T \to S)$ --- from 4), 9) and 27) discharging assumptions [a] and [c]


$(\lnot T \lor P) \to (T \to S)$ --- from 4) and 28) by $(\to \text I)$.


Here is an alternative proof that uses Disjunctive syllogism:


*$(¬T ∨ P)$ --- Assumption


*$T$ --- assumed [a]


*$P$ --- from 4) and 5)
Now we insert lines 10)-26) above to get:


*$S$
and we conclude with:

$T \to S$ --- from 5) and 27) by $(\to \text I)$, discharging [a]

A: The premise is a negation $\neg(S \to \neg P)$, so it is likely you need to perform negation elimination. For that you need to intermediately derive $S \to \neg P$, resulting in a contradiction from which you may infer anything.
That anything will be $S$, so you prove the conclusion by contradiction, assuming $\neg S$ earlier on and dropping that assumption in the last step.
Now you want to derive $S \to \neg P$; this is an implication, so you have to derive $\neg P$ from an assumption $S$. Given the other assumptions you have at your disposal, how do you think that subderivation can be plugged together?
A: $\def\fitch#1#2{~~\begin{array}{|l|}\hline #1\\\hline#2\\\hline\end{array}~~}$
You seek to derive $S$ under the assumption of $T$, $\lnot T\vee P$, and the premises.
You can immediately derive $P$ and $Q$ using disjunctive syllogism and modus ponens.
Likewise you could there after derive $\neg R$ and $\neg(S\to\neg P)$ using modus tollens.
However, I'd rather use reduction to absurdity to derive $S$.
Discharge the necessary contradictions and you are done.
$$\fitch{~~1.~P\to Q\\~~2.~R\to\lnot Q\\~~3.~(S\to\lnot P)\to R}{\fitch{~~4.~\lnot T\lor P}{\fitch{~~5.~T}{~~6.~P\\~~7.~Q\\\fitch{~~8.~\lnot S}{\vdots\\14.~\lnot Q}\\15.~S}\\16.~T\to S}\\17.~(\lnot T\lor P)\to(T\to S)}$$
Using logic.tamu.edu/daemon.html
P->Q, R->~Q, (S->~P)->R |- (~TvP)->(T->S)
OK    1          (1)   P->Q           A         
OK    2          (2)   R->~Q          A         
OK    3          (3)   (S->~P)->R     A         
OK    4          (4)   ~TvP           A         
OK    5          (5)   T              A         
OK    4,5        (6)   P              4,5vE     
OK    1,4,5      (7)   Q              1,6->E    
OK    8          (8)   ~S             A         
:     :          :     :              :
OK    2,3,8      (14)  ~Q             ..,..->E   
OK    1,2,3,4,5  (15)  S              7,14RAA(8)
OK    1,2,3,4    (16)  T->S           15->I(5)  
OK    1,2,3      (17)  (~TvP)->(T->S) 16->I(4)  

