Is this a valid natural deduction? I'm trying to prove that $\{(p_1\implies p_2),p_1,(p_2\implies p_3)\}\vdash (p_3\vee p_5)$ which seems easy, but I'm unsure about a step in the way.
I did:
$1.\ p_1\implies p_2 \text{  (Pre)}\\2.\ p_1 \text{(Pre)}\\3. \ p_2\implies p_3 \text{(Pre)}\\ 4.\ p_2 \text{ (By 2. and 1.)}\\ 5.\ p_3 \text{(By 4. and 3.)} \\ 6.\ \neg(p_3\vee p_5) \text{ (Assume)}\\ 6.1.\ (\neg p_3\wedge \neg p_5) \text{(By Morgan)}\\6.2. \ \neg p_3\text{ (By 6.2)}\\7. \ (p_3\vee p_5) \text{ (By contradiction of 6.)}$
Is this right?. I'm unsure about the step 6 where $p_5$ comes from nowhere, should I assume $p_5$ first?

There doesn't seem to be anything strictly wrong with your strategy -- assumptions don't have to come from anywhere as long as they get properly discharged.
But it seems to be a detour. Most natural deduction systems have a rule that allows you to infer directly from $P$ to $P\lor Q$. Doesn't yours?
On the other hand, most natural deduction systems don't include De Morgan's rules as primitive inferences. Are you sure your step from 6 to 6.1 is formally allowed?
