Inference Proof for Biconditional I'm asked to prove $(p\rightarrow (q \vee r)) \leftrightarrow ((p \wedge \neg q)\rightarrow r)$ using inference rules and I'm not quite sure how to do it. This is what I have so far.
$1 [(p \wedge \neg q) \rightarrow r]\quad$ assume
$2 \space (p) \space\quad\wedge$-elimination (1)
$3 \space (\neg q) \space\quad \wedge$-elimination(1)
$4\space [r] \quad$ assume
$5 \space (q \vee r)$ $\quad\vee$-intro(3,4)
$6 \space(p \rightarrow(q\vee r)) \quad\rightarrow$-intro (2,6)
This only proves the biconditional one way (and I'm not even sure if its correct) and I don't know where to go from here.
 A: Proving $A \leftrightarrow B$ amounts to prove both $A \to B$ and $B \to A$. I will prove both of them using classical natural deduction, which seems to be the formal system you know. Given an inference rule $r$, I will use the notation 
\begin{align}
\dfrac{A_1 \ \dots \ A_n}{B}r
\end{align}
which means that given the premises $A_1, \dots, A_n$, you can infer the conclusion $B$ by means of the inference rule $r$. So, a derivation in classical natural deduction will be a tree-like concatenation of inference rules in this notation.
Let us prove that $(p\rightarrow (q \vee r)) \to ((p \wedge \neg q)\rightarrow r)$: assume $(p\rightarrow (q \vee r))$, let us prove $((p \wedge \neg q)\rightarrow r)$
\begin{align}
\dfrac{\dfrac{\dfrac{p \!\to\! (q \lor r) \quad \dfrac{[p \land \lnot q]^2}{p}\land_e}{q \lor r}\to_e \qquad \dfrac{\dfrac{\dfrac{[p \land \lnot q]^2}{\lnot q}\land_e \qquad [q]^1}{\bot}\lnot_e}{r}\bot_e \qquad [r]^1}{r}\lor_e^1}{(p \land \lnot q) \to r}\to_i^2
\end{align}
Now, let us prove that $((p \wedge \neg q)\rightarrow r) \to (p\rightarrow (q \vee r))$: assume $(p \land \lnot q) \to r$ and let us prove $p \to (q \lor r)$
\begin{align}
\dfrac{\dfrac{q \lor \lnot q \qquad \dfrac{[q]^1}{q \lor r}\lor_{i_L} \qquad \dfrac{\dfrac{(p \land \lnot q) \to r \qquad \dfrac{[p]^2 \qquad [\lnot q]^1}{p \land \lnot q}\land_i}{r}\to_e}{q \lor r}\lor_{i_R}}{q \lor r}\lor_e^1}{p \to (q \lor r)}\to_i^2
\end{align}
where $q \lor \lnot q$ is provable in classical natural deduction as follows:
\begin{align}
\dfrac{\dfrac{[\lnot (q \lor \lnot q)]^2 \qquad \dfrac{\dfrac{\dfrac{[\lnot (q \lor \lnot q)]^2 \qquad \dfrac{[q]^1}{q \lor \lnot q}\lor_{i_L}}{\bot}}{\lnot q}\lnot_i^1}{q \lor \lnot q}\lor_{i_R}}{\bot}\lnot_e}{q \lor \lnot q}\text{raa}^2
\end{align}
A: 
1 $[(p∧¬q)→r]$ assume
2 $(p)$ ∧ elimination (1)

No, you cannot eliminate from the antecedant of an implication.   This is another assumptions.   Preferred format would be to indent or otherwise indicate the start of a sub proof (well, I guess you're trying that with the []-brackets.)   An assumption has been made and will later need to be discharged.

3 $(¬q)$ ∧ elimination(1)

Again, you cannot $\wedge$-eliminate from the antecedant of an implication.   You need $\land$ to be the highest priority in the order of operations. In statement $1$, it is $\to$ that has operational precedence.
This is actually an assumption.

4 $[r]$ assume

You are not actually assuming this; you appear to be using $\to$ elimination from the prior assumptions: $\{p\wedge \neg q, (p\wedge \neg q)\to r \}~\vdash~r$
Of course, you also missed the step where you used $\wedge$ introduction (not elimination) to obtain $p\wedge\neg q$ from the two preceeding assumptions.

5 $(q∨r)$ ∨ intro(3,4)

This you have correct, almost, you just need line 4 to obtain this,  $r\vdash q\vee r$

6 $(p→(q∨r))$ → intro (2,6)

Unfortunately with the assumption in line 3 you have $p\to (\neg q\to (q\vee r))$
Before this you should perhaps have used LEM and a $\vee$-elimination to discharge assumptions $q$ and $\neg q$ (since $q\vdash q\vee r$ by $\vee$ introduction also).

$\def\fitch#1#2{{\quad\begin{array}{|l}#1\\\hline#2\end{array}}}$
You seek to demonstrate that when given the premise of $(p\wedge \neg q)\to r$, assuming $p$ will infer $q\vee r$, thus deducing $p\to(q\vee r)$.   So do just that.   I'd have suggested proof by contradiction, but LEM works too if allowed.
$\fitch{}{\fitch{1\quad (p\wedge\neg q)\to r\qquad\text{assumption}}{\fitch{2\quad p\qquad\text{assumption}}{\fitch{3\quad \neg q\qquad\text{assumption}}{4\quad p\wedge\neg q\qquad\text{conjunction introduction, 2,3}\\5\quad r\qquad\text{conditional elimination, 1,4}\\6\quad q\vee r\qquad\text{disjunction introduction, 5}}\\7\quad\neg q\to (q\vee r)\qquad\text{conditional introduction 3,6}\\\fitch{8\quad q\qquad\text{assumption}}{9\quad q\vee r\qquad\text{disjunction introduction, 8}}\\10\quad q\to(q\vee r)\qquad\text{conditional introduction, 8,9}\\11\quad q\vee\neg q\qquad\text{principle of excluded middle}\\12\quad q\vee r\qquad\text{disjunction elimination, 7, 10, 11}}\\13\quad p\to(q\vee r)\qquad\text{conditional introduction, 2,12}}\\14\quad ((p\wedge\neg q)\to r)~\to~(p\to(q\vee r))\qquad\text{conditional introduction, 1, 13}}$
For the other direction, demonstrate that under the premise of $p\to(q\vee r)$ that assuming $p\wedge\neg q$ will infer $r$, thus deducing $(p\wedge\neg q)\to r$
$$\fitch{}{\fitch{1\quad p\to( q\vee r)}{\fitch{2\quad p\wedge\neg q}{\vdots\\\cdot\quad r}\\\cdot\quad (p\wedge\neg q)\to r}\\\cdot\quad(p\to( q\vee r))~\to~((p\wedge\neg q)\to r)}$$
