How would you go about long conditional proofs? So, I've had problems similar to this, but this problem is way larger than I'm used to, and I'm not sure how to go about this. What do I assume? I want to assume $p \land q$, but then what? 
Show  the  following  using  conditional  proof.    You  may  assume  associativity  and commutativity,  and  you  may  use  generalized  forms  of  laws  and  rules. Justify  each  step,  but you need not show the substitutions used in applying laws and rules.
$$p \to (s \to t), \lnot q \lor r, p\land q \land r \to u \vdash p \land q \to (\lnot r \lor s \to t \land u)$$
 A: It looks like you're allowed to use the deduction theorem that is you're almost done if you can prove:
$$p \to (s \to t), \lnot q \lor r, p\land q \land r \to u, p \land q \vdash \lnot r \lor s \to t \land u$$
and that is almost done if you prove 
$$p \to (s \to t), \lnot q \lor r, p\land q \land r \to u, p \land q, \lnot r \lor s \vdash t \land u$$
What we want to use is the fact that $\neg\phi\lor\psi$ is the same ase $\phi\rightarrow\psi$, that way we get that from the assumptions that we know that both $p$ and $q$ (from $p\land q$) which via implications leads to $t$ and $u$. The rest is to put this into symbolics, first we deduce $t$:
$$\begin{align}
\tag{1}p \to (s \to t), \lnot q \lor r, p\land q \land r \to u, p \land q, \lnot r \lor s & \vdash p\land q & \text{premise}\\
\tag{2}p \to (s \to t), \lnot q \lor r, p\land q \land r \to u, p \land q, \lnot r \lor s & \vdash p &\text{conjunction elimination form (1)}\\
\tag{3}p \to (s \to t), \lnot q \lor r, p\land q \land r \to u, p \land q, \lnot r \lor s & \vdash p \to (s\to t)&\text{premise}\\
\tag{4}p \to (s \to t), \lnot q \lor r, p\land q \land r \to u, p \land q, \lnot r \lor s & \vdash s \to t&\text{modus ponens using (2) and (3)}\\
\tag{5}p \to (s \to t), \lnot q \lor r, p\land q \land r \to u, p \land q, \lnot r \lor s & \vdash q &\text{conjunction elimination using (2)}\\
\tag{6}p \to (s \to t), \lnot q \lor r, p\land q \land r \to u, p \land q, \lnot r \lor s & \vdash \neg\neg q&\text{double negation using (5)}\\
\tag{7}p \to (s \to t), \lnot q \lor r, p\land q \land r \to u, p \land q, \lnot r \lor s & \vdash \neg q\lor r&\text{premise}\\
\tag{8}p \to (s \to t), \lnot q \lor r, p\land q \land r \to u, p \land q, \lnot r \lor s & \vdash r&\text{disjunctive syllogism using (6) and (7)}\\
\tag{9}p \to (s \to t), \lnot q \lor r, p\land q \land r \to u, p \land q, \lnot r \lor s & \vdash \neg\neg r&\text{double negation}\\
\tag{10}p \to (s \to t), \lnot q \lor r, p\land q \land r \to u, p \land q, \lnot r \lor s & \vdash \neg r\lor s&\text{premise}\\
\tag{11}p \to (s \to t), \lnot q \lor r, p\land q \land r \to u, p \land q, \lnot r \lor s & \vdash s&\text{disjunctive syllogism using (9) and (10)}\\
\tag{12}p \to (s \to t), \lnot q \lor r, p\land q \land r \to u, p \land q, \lnot r \lor s & \vdash t&\text{modus ponens using (11) and (4)}\\
\end{align}$$
We can also stright forwardly deduce $u$:
$$
\begin{align}
\tag{13}p \to (s \to t), \lnot q \lor r, p\land q \land r \to u, p \land q, \lnot r \lor s & \vdash p&\text{repetition of (2)}\\
\tag{14}p \to (s \to t), \lnot q \lor r, p\land q \land r \to u, p \land q, \lnot r \lor s & \vdash q&\text{repetition of (5)}\\
\tag{15}p \to (s \to t), \lnot q \lor r, p\land q \land r \to u, p \land q, \lnot r \lor s & \vdash r&\text{repetition of (8)}\\
\tag{16}p \to (s \to t), \lnot q \lor r, p\land q \land r \to u, p \land q, \lnot r \lor s & \vdash (p\land q\land r)&\text{conjunction introuduction using (13), (14) and (15)}\\
\tag{17}p \to (s \to t), \lnot q \lor r, p\land q \land r \to u, p \land q, \lnot r \lor s & \vdash (p\land q\land r)\to u&\text{premise}\\
\tag{18}p \to (s \to t), \lnot q \lor r, p\land q \land r \to u, p \land q, \lnot r \lor s & \vdash u&\text{modus ponens using (16) and (17)}\\
\end{align}
$$
Now we only have to wrap it up using the deduction theorem.
$$
\begin{align}
\tag{19}p \to (s \to t), \lnot q \lor r, p\land q \land r \to u, p \land q, \lnot r \lor s & \vdash u \land v&\text{conjunction introduction using (12) and (18)}\\
\tag{20}p \to (s \to t), \lnot q \lor r, p\land q \land r \to u, p \land q &\vdash \lnot r \lor s \to u \land v&\text{deduction theorem using (19)}\\
p \to (s \to t), \lnot q \lor r, p\land q \land r \to u &\vdash p \land q \to (\lnot r \lor s \to u \land v)&\text{deduction theorem using (20)}\\
\end{align}
$$
A: The sought conclusion:

$p∧q→(¬r∨s→t∧u)$

is a conditional; thus, the "strategy" is to assume the antecedent and use it to "unpack" the premises:
1) $p \land q$ --- assumed [a].
From it, by $\land$E, we derive the conjuncts :$p$ and $q$ and then we can use $p$ to derive:
2) $s→t$ --- from 1st premise: $p→(s→t)$ and 1) by $\to$E.
But also the consequent of the sought conclusion is a conditional: $¬r∨s → t∧u$ and we need some of its "components" to go on. So, new assumption:
3) $¬r∨s$ --- assumed [b].
It is a disjunction, and thus we have to use $\lor$E (proof by cases).
First case (outer $\lor$E):
4) $s$ --- assumed [c] for $\lor$E.
5) $t$ --- from 2) and 4) by $\to$E.
Now use $\lor$E again with 2nd premise: $¬q∨r$.
First case (inner $\lor$E)
6) $r$ --- assumed [d] for $\lor$E.
7) $p \land q \land r$ --- from 1) and 6) by $\land$I
8) $u$ --- from 3rd premise: $p∧q∧r → u$ and 7) by $\to$E
9) $t∧u$ --- from 5) and 8) by $\land$I.
One "path" has been completed; now we have to do the same for all others "open path" due to the two nested $\lor$E, in order to derive $t \land u$ in all cases.
Having done that, we go on with:
10) $(¬r∨s) \to (t∧u)$ --- from 3) and 9) by $\to$I (Conditional Proof), discharging [b]

11) $p∧q→(¬r∨s→t∧u)$ --- from 1) and 10) by $\to$I (Conditional Proof), discharging [a].

