To answer your question on infinitude of primes properly, one would need to set up a very restrictive and strict version of the area of mathematical logic known as reverse mathematics. (This is partly because the question asks for arithmetical consequences of a second order statement.) This strict setting has not been developed/studied yet.
Traditional research in reverse mathematics builds on the basis of a theory called $RCA_0$; adding to it a weak version of König's Lemma (stating that every infinite subtree of the full binary tree has a branch) results in a system denoted $WKL_0$, which is strictly stronger and has been extensively studied. $RCA_0$ is a very weak system, but proves the infinitude of primes and much more.
The study of weak systems of first order arithmetic is also a very extensively studied area, but the mixture of the two is at its infancy, as far as I know.
As for the question regarding the prime ideal theorem, we can do better, at least in terms of the classical version of König's Lemma: $WKL_0$ suffices to prove that every countable commutative ring has a prime ideal. This is as far as we can expect, as we are limited by the language of second order arithmetic, so the rings we can study are countable.
Let me add a slightly technical remark on why answering the question looks difficult. For formal investigations involving the natural numbers, there is a bare minimum we need to adopt to be able to talk of arithmetic, namely the theory $Q$ of Robinson arithmetic. Strengthening this fragment is usually achieved by assuming induction for certain classes of formulas. For example, $I\Delta_0$ assumes induction for bounded formulas. The study of theories in the neighborhood of $I\Delta_0$ is the topic of bounded arithmetic, see for example the work of Sam Buss. It is still open whether $I\Delta_0$ suffices to prove the infinitude of primes, but just a bit more suffices (for example, $I\Delta_0$ plus a version of the pigeonhole principle).
To properly address your problem, we would need to work over a theory consisting of a suitable formalization of König's Lemma (a second order principle), and a first order fragment around the level of $I\Delta_0$, if not weaker. This leaves us almost without any coding devices. The adoption of König's Lemma should help to make up for this weakness, but on the other hand, there seem to be very few trees we could build in such a setting to which the Lemma would apply.
The problem looks interesting, and the appropriate setting for this work should be an extension of what is now called bounded reverse mathematics.
(You may also be interested in this MO question on formalizing proofs of the infinitude of primes.)