In the (short) book [J] "Notes on logic and set theory" (Peter Johnstone).
The author P.J. considered the first order Peano language of naturals (the $\bar{0}$, the successor $S$, $+$, $\cdot$) and the PA theory (inductive usual condiction on addiction and moltiplication, and a system of inductive axioms for each formula), see [J] p. 29.
in the last chapter 9, he define the Godel coding of PA language: $\sharp X\in N$ (X a term or formula ecc.) and define the relation (on couples of natural numbers):
$Ded_N(n, m):: $ if $n= \sharp (p_1,\ldots p_n)$ where $(p_1,\ldots p_n)$ is a proof of a proposition $q=p_n$ and $m=\sharp q$.
this relation is recursive, this mean that its characteristic funtion is recursive, then there is a formula $D(x, y,z)$ that $PA$-define it ([J] p. 50, T.4.13).
Define the $PA$ formula $Def(x, y):=D(x, y, z)[z/1]$
we have $Def(\bar{n}, \bar{m})$ iff $Def_N(n, m)$, where $\bar{n}$ is the usual close term of the language, like a formal copy of $n$ .
Define $Th(y):=\exists x: Ded(x, y)$ ("mean" that $y$ is a code of a theorem of $PA$, in the $PA$ language).
Suppose that $PA\vdash p\to q$, then from a code $n$ of a proof of $p$ we can make (in recursive term) a code $\tilde{n}$ of a proof of $q$ (just add to the proof the elements $p\to q, q$ and recodifing)
P.J. claim that this idea can be formalized, precisely he claim that: if $PA\vdash p\to q\ $ then $\ PA\vdash\ Th(\sharp p)\to Th(\sharp q)$.
although it seems obvious and natural, havent reach a formal syntactically exact proof of it, and haven't found examples of it in the bibliography known to me.
Could you help me?