For the question in the body: Yes, any provable formula of whatever complexity is logically equivalent (given the axioms it is proved from) to $0=0$, which is even $\Delta_0^0$.
(Unless the logic the "proof" is done in is unsound, of course).
For the question in the title: No, such a mechanical procedure cannot exist, because if it did, we could use it to decide logical equivalence in general.
Suppose $\psi$ is a sentence and we want to know whether it is provable. Apply your hypothetical procedure to
$$\phi(x)\;\equiv\; \psi\land (x=x)$$
Now, it $\psi$ is provable, then the output of your procedure must be a $\Delta_0^0$ formula that is true for $x=0$, and checking that is a simple mechanical matter. Conversely if $\phi$ is logically equivalent to a $\Delta_0^0$ formula that is true for $x=0$, then by Gödel's completeness theorem, $\psi$ must be is provable.
In the comment below you amend the question so it is not about "provably equivalent in PA", but "semantically equivalent in the actual natural numbers". That's actually even worse from a decidability point of view -- truth about $\mathbb N$ is if anything more slippery than provability in PA.
A mechanical procedure for simplifying formulas behaves enough like a proof system that Gödel's incompleteness theorem applies to it, and we get:
Theorem. Let $P$ be some mechanical procedure which transforms arithmetical formulas into arithmetical formulas. Assume that the output of $P$ is always semantically equivalent (in $\mathbb N$) to the input. Then there exists a formula which $P$ does not transform into a semantically equivalent formula on the lowest possible level in the arithmetical hierarchy.
Proof. Call a sentence $\phi$ "good" if $P(\phi)$ is a $\Delta^0_0$ sentence that is true. (This concept of "goodness" will take the place of "provable" in our analogy to Gödel).
Our strategy will be to produce a $\phi$ that is true but not good. Then whatever $P(\phi)$ is, it has to be something that is true, because we're assuming $P$ preserves semantics. However, $P(\phi)$ cannot be $\Delta^0_0$, because then $\phi$ would be good, which it isn't. But then $P(\phi)$ must belong somewhere higher in the arithmetical hierarchy, which means that $\phi$ is a formula for which $P$ does not produce output of minimal complexity.
In order to find such a $\phi$, introduce Gödel numbers for formulas in the usual way. Since $P$ is a mechanical procedure, and the property of being a true $\Delta^0_0$ sentence is computable, by Church-Turing and other well-known stuff there is an arithmetical formula $\psi(x)$ that is true exactly when $x$ is the Gödel number of a good formula.
Following Gödel, we can then diagonalize and produce a sentence $\phi$ whose intuitive meaning is "I am not good". (Details of this diagonalization omitted; they are somewhat confusing, not particularly enlightening, and can be found in any good exposition of Gödel's proof).
I claim that $\phi$ is not good. Namely, assume to the contrary that $\phi$ is good. Then by our assumptions on $P$, $\phi$ must be semantically equivalent to true formula -- but then $\phi$ must itself be true, and since it asserts that $\phi$ is not good, we have reached a contradiction.
Therefore $\phi$ is not good. But since that is just what $\phi$ asserts, that means that $\phi$ is true! Q.E.D.
(Essentially the same argument works if you stipulate only that $P$ preserves semantics of formulas with exactly one free variable -- just add in a vacuous "$\cdots\land(x=x)$" at appropriate places in the argument, then).