# Is my proof by natural deduction for $\vdash (p\rightarrow(q\wedge r))\rightarrow((p\rightarrow q)\wedge(p\rightarrow r))$ correct?

1. $\quad\bullet\;p\rightarrow\left(q\wedge r\right)$ --- Assumption
2. $\quad\bullet\quad\bullet\; p$ --- Assumption
3. $\quad\bullet\quad\bullet\; q\wedge r$ --- $\rightarrow$ Elim 1,2
4. $\quad\bullet\quad\bullet\; q$ --- $\wedge$ Elim 3
5. $\quad\bullet\quad\bullet\; r$ --- $\wedge$ Elim 3
6. $\quad\bullet\; p\rightarrow q$ --- $\rightarrow$ Intro 2,4
7. $\quad\bullet\; p\rightarrow r$ --- $\rightarrow$ Intro 2,5
8. $\quad\bullet\;\left(p\rightarrow q\right)\wedge\left(p\rightarrow r\right)$ --- $\wedge$ Intro 6,7
9. $\;\left(p\rightarrow\left(q\wedge r\right)\right)\rightarrow\left(\left(p\rightarrow q\right)\wedge\left(p\rightarrow r\right)\right)$ --- $\rightarrow$ Intro 1,8

I'm concerned about introducing two implications(6 & 7) from same subproof.

• I don't think there is any problem with introducing two implications from the same subproof. – Kenny Lau Sep 14 '17 at 5:07

Semantically that is of course perfectly valid, and it is indeed no problem in most formal proof systems!

Well, of course you can do it without introducing two implications from the same subproof:

1. $\quad\bullet\;p\rightarrow\left(q\wedge r\right)$ --- Assumption
2. $\quad\bullet\quad\bullet\; p$ --- Assumption
3. $\quad\bullet\quad\bullet\; q\wedge r$ --- $\rightarrow$ Elim 1,2
4. $\quad\bullet\quad\bullet\; q$ --- $\wedge$ Elim 3
5. $\quad\bullet\; p\rightarrow q$ --- $\rightarrow$ Intro 2-4
6. $\quad\bullet\quad\bullet\; p$ --- Assumption
7. $\quad\bullet\quad\bullet\; q\wedge r$ --- $\rightarrow$ Elim 1,6
8. $\quad\bullet\quad\bullet\; r$ --- $\wedge$ Elim 3
9. $\quad\bullet\; p\rightarrow r$ --- $\rightarrow$ Intro 6-8
10. $\quad\bullet\;\left(p\rightarrow q\right)\wedge\left(p\rightarrow r\right)$ --- $\wedge$ Intro 5,9
11. $\;\left(p\rightarrow\left(q\wedge r\right)\right)\rightarrow\left(\left(p\rightarrow q\right)\wedge\left(p\rightarrow r\right)\right)$ --- $\rightarrow$ Intro 1-10

The OP is concerned with the following:

I'm concerned about introducing two implications(6 & 7) from same subproof.

Here is a proof checker that accepts those two implications from the same subproof.

Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/

P. D. Magnus, Tim Button with additions by J. Robert Loftis remixed and revised by Aaron Thomas-Bolduc, Richard Zach, forallx Calgary Remix: An Introduction to Formal Logic, Winter 2018. http://forallx.openlogicproject.org/