Consider a natural deduction proof system. Suppose I know that $\vdash \phi$ (the sentence $\phi$ is provable from no premises). If I'm proving something like $\vdash \psi$, can I just use that $\phi$ is valid? And similarly, if I know that $\phi'\vdash \phi''$, can I use this when proving $\psi$? For example, if I know that $p\to q\vdash \neg q\to \neg p$ and $A\vdash \neg p$, then is this proof of the fact that $\vdash A\to (p\to q)$ is correct?
0. (no premises) 1.A (assumption) 2.not(q) (assumption) 3.not(p) (here we use that A proves not(p)) 4.not(q) → not(p) (from 2,3) 5.p → q (from 4; here we use that not(q) → not(p) proves p → q) 6.A → (p → q) (from 1,5)
If so, how do I justify formally that what was done in lines 3 and 5 is legit?