# 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?

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 this does show that if one considers a system with the rules used in the proof analysis of the OP's proof, that left-disjunction introduction becomes a derivable rule of inference. One might argue that it should be a derivable rule of inference, since from just conditional introduction and conditional elimination we have p $\vdash$ CCpqq, and since the truth table for CCpqq and Apq match, we can think of this as implying that left-disjunction introduction is a valid rule of inference. – Doug Spoonwood Jul 22 '14 at 4:24