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

Question

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.

Answer 1

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

Answer 2

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