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

*$\quad\bullet\;p\rightarrow\left(q\wedge r\right)$ --- Assumption

*$\quad\bullet\quad\bullet\; p$ --- Assumption

*$\quad\bullet\quad\bullet\; q\wedge r$ --- $\rightarrow$ Elim 1,2

*$\quad\bullet\quad\bullet\; q$ --- $\wedge$ Elim 3

*$\quad\bullet\quad\bullet\; r$ --- $\wedge$ Elim 3

*$\quad\bullet\; p\rightarrow q$ --- $\rightarrow$ Intro 2,4

*$\quad\bullet\; p\rightarrow r$ --- $\rightarrow$ Intro 2,5

*$\quad\bullet\;\left(p\rightarrow q\right)\wedge\left(p\rightarrow r\right)$ --- $\wedge$ Intro 6,7

*$\;\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.
 A: Semantically that is of course perfectly valid, and it is indeed no problem in most formal proof systems!
A: Well, of course you can do it without introducing two implications from the same subproof:


*

*$\quad\bullet\;p\rightarrow\left(q\wedge r\right)$ --- Assumption

*$\quad\bullet\quad\bullet\; p$ --- Assumption

*$\quad\bullet\quad\bullet\; q\wedge r$ --- $\rightarrow$ Elim 1,2

*$\quad\bullet\quad\bullet\; q$ --- $\wedge$ Elim 3

*$\quad\bullet\; p\rightarrow q$ --- $\rightarrow$ Intro 2-4

*$\quad\bullet\quad\bullet\; p$ --- Assumption

*$\quad\bullet\quad\bullet\; q\wedge r$ --- $\rightarrow$ Elim 1,6

*$\quad\bullet\quad\bullet\; r$ --- $\wedge$ Elim 3

*$\quad\bullet\; p\rightarrow r$ --- $\rightarrow$ Intro 6-8

*$\quad\bullet\;\left(p\rightarrow q\right)\wedge\left(p\rightarrow r\right)$ --- $\wedge$ Intro 5,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-10

A: 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/
