Formal Fitch Proof and Inference Rules 
So I was given the following assignment and the way I had this problem solved involves dis-junction syllogism but I just realized Fitch system doesn't have this. Is there an alternative form to solving the problem or citing line number 9? 
 A: In Fitch you'll need to take several steps to derive $P$ from $R \lor P$ and $\neg R$:
$\def \fitch#1#2{\begin{array}{|l}#1 \\ \hline #2 \end{array}}$
$\fitch{
1. R \lor P\\
2. \neg R
}{
\fitch{
3. R}{
4. \bot \quad \bot \ Intro \ 2,3\\
5. P \quad \bot \ Elim \ 4}\\
\fitch{
6. P}{
7. P \quad Reit}\\
8. P \quad \lor \ Elim \ 1,3-5,6-7}$
A: Indeed, $r\vee p, \neg r\vdash p$ is not an elementary rule of inference in Fitch's System.   However, it is provable.
$$\begin{array}{rll}
8 & \vert\quad\vert\quad \neg r &&\text{Assumption}\\[-1ex]
8.1& \vert\quad\vert\quad r\vee p & 4,&\text{Reiteration}\\[-1ex]
8.2& \vert\quad\vert\quad\vert\quad r & &\text{Assumption}\\[-1ex]
8.3& \vert\quad\vert\quad\vert\quad \neg r & 8,&\text{Reiteration}\\[-1ex]
8.4& \vert\quad\vert\quad\vert\quad \bot & 8.2,8.3,&\text{Contradiction Introduction}\\[-1ex]
8.5& \vert\quad\vert\quad\vert\quad p & 8.4,&\text{Contradiction Elimination}\\[-1ex]
8.6& \vert\quad\vert\quad \neg r\to p & 8.2,8.5,&\text{Conditional Introduction}\\[-1ex]
8.7& \vert\quad\vert\quad\vert\quad p & &\text{Assumption}\\[-1ex]
8.8& \vert\quad\vert\quad\vert\quad p & 8.7,&\text{Reiteration} \\[-1ex]
8.9& \vert\quad\vert\quad p\to p & 8.7,8.8,&\text{Conditional Introduction}\\[-1ex]
9 & \vert\quad\vert\quad p & 8.1,8.6,8.9,&\text{Disjunctive Elimination}& 4,8,&\text{Disjunctive Syllogism}\\[-1ex]\vdots
\end{array}$$
$\newcommand{\noshow}[1]{} 
\noshow{\begin{array}{r|l:rl} 1& s \to r\vee p & &\text{Premise} \\[-1ex]
2 & p\to(\neg r\to q)& &\text{Premise}\\[-1ex]
3 & \vert\quad s & &\text{Assumption}\\[-1ex]
4 & \vert\quad r\vee p & 1,3,&\text{Conditional Elimination}\\[-1ex]
5 & \vert\quad\vert\quad r & &\text{Assumption}\\[-1ex]
6 & \vert\quad\vert\quad q\vee r & 5,&\text{Disjunctive Introduction}\\[-1ex]
7 & \vert\quad r\to q\vee r & 5,6,&\text{Conditional Introduction}\\[-1ex]
8 & \vert\quad\vert\quad \neg r &&\text{Assumption}\\[-1ex]
8.1& \vert\quad\vert\quad r\vee p & 4,&\text{Reiteration}\\[-1ex]
8.2& \vert\quad\vert\quad\vert\quad r & &\text{Assumption}\\[-1ex]
8.3& \vert\quad\vert\quad\vert\quad \neg r & 8,&\text{Reiteration}\\[-1ex]
8.4& \vert\quad\vert\quad\vert\quad \bot & 8.2,8.3,&\text{Contradiction Introduction}\\[-1ex]
8.5& \vert\quad\vert\quad\vert\quad p & 8.4,&\text{Contradiction Elimination}\\[-1ex]
8.6& \vert\quad\vert\quad \neg r\to p & 8.2,8.5,&\text{Conditional Introduction}\\[-1ex]
8.7& \vert\quad\vert\quad\vert\quad p & &\text{Assumption}\\[-1ex]
8.8& \vert\quad\vert\quad\vert\quad p & 8.7,&\text{Reiteration} \\[-1ex]
8.9& \vert\quad\vert\quad p\to p & 8.7,8.8,&\text{Conditional Introduction}\\[-1ex]
9 & \vert\quad\vert\quad p & 8.1,8.6,8.9,&\text{Disjunctive Elimination}& 4,8,&\text{Disjunctive Syllogism}\\[-1ex]
10 & \vert\quad\vert\quad \neg r\to q &2,9,&\text{Conditional Elimination}\\[-1ex]
11 & \vert\quad\vert\quad q & 8,11,&\text{Conditional Elimination}\\[-1ex]
12 & \vert\quad\vert\quad q\vee r & 11,&\text{Disjunctive Introduction}\\[-1ex]
13 & \vert\quad \neg r\to q\vee r &8,12,&\text{Conditional Introduction}\\[-1ex]
14 & \vert\quad r\vee\neg r & &\text{Law of Excluded Middle}\\[-1ex]
15 & \vert\quad q\vee r & 7,13,14,&\text{Disjunctive Elimination}\\[-1ex]
16 & s\to q\vee r & 3,15,&\text{Conditional Elimination}
\end{array}}$
