Deriving $\neg R$ from $\{R↔(R∨(P∧¬P)), R↔¬P, ¬P→(P↔(Q→Q)), P→Q\}$ 
Give a derivation of $\neg R$ from the following premises:
$$\{R\leftrightarrow(R\lor(P\land \neg P)), R\leftrightarrow\neg P, \neg P\to(P\leftrightarrow(Q\to Q)), P\to Q\}$$
using the rules found here.

I don't know where to start...
Edit:

1 1) R↔(R/lor(P∧¬P)) P
2 2) R↔¬P P
3 3) ¬P→(P↔(Q→Q))  P
4 4)P→Q P
5 5)R P
2 6)R→¬P  2,BE
2,5 7)¬P 5,6,MP
2,3 8)P↔(Q→Q) 3,7,MP
2,3 9)(Q→Q)→P 8,BE
2,3,5 10)¬(Q→Q) 7,9,MT
2,3,5 11)Q∧¬Q 10,NC
2,3,5 12)Q 11,simp
2,3,5 12)¬Q 11,simp
2,3 14)¬R 12,13,RAA
2,15)¬R 5,14,RAA

 A: Your premises are:


*

*$R \leftrightarrow (R \lor (P \land \lnot P))$

*$R \leftrightarrow \lnot P$

*$\lnot P \rightarrow (P \leftrightarrow (Q \rightarrow Q))$

*$P \rightarrow Q$


You want to prove $\lnot R$, so suppose, for contradiction, that $R$. That with (2) gives us $\lnot P$, which with (3) gives us $(P \leftrightarrow (Q \rightarrow Q))$, which implies that $((Q \rightarrow Q) \rightarrow P)$. This with $\lnot P$ gives us $\lnot (Q \rightarrow Q)$ $\equiv \lnot (\lnot Q \lor Q) \equiv \lnot (\top) \equiv \bot$. Therefore we conclude that $\lnot R$.
That's just a sketch. I've used proof by contradiction, $\leftrightarrow$-elimination, the definition of '$\leftrightarrow$', modus tollens, modus ponens, the definition of '$\rightarrow$', and the fact that $(\lnot Q \lor Q)$ is a tautology. Let me know if you're having trouble adapting it to Chellas' system. It shouldn't be too difficult. For example, $\leftrightarrow$-elimination is called 'BE' there, modus tollens has the suggestive 'MT' label, and so on.
A: Yes, it all looks, roughly speaking, good. 
But for stylistic purposes, you usually want to call your "P (premise)": which you introduce on line $5$, an assumption. So $R$ is an assumption "A". Indent the assumption and the sub-proof of all that follows from the assumption, $5$, until and including your arrival at the contradiction, RAA.  
You can also introduce RAA immediately after obtaining $Q \land \lnot Q$ which forms your contradiction $\perp$. Then your subproof ends, and you can conclude $\lnot R$. Some proof systems refer to the invocation of $\lnot R$ as "negation introduction".  That is, you need only one invocation of RAA.
