Indeed, and one can give specific metatheorems in this direction:
For instance, regarding statements of the form "for all natural numbers x, there is a natural number y such that %", where in "%" no further quantifiers appear, there is no difference between ZFC (Zermelo–Fraenkel set theory with the axiom of choice), ZF (set theory without the axiom of choice) and IZF (set theory without the axiom of choice and without the law of excluded middle).
Any ZFC-proof of such a statement can be mechanically transformed to an IZF-proof, with just a modest increase in proof length.
For instance, regarding statements of the form "for all natural numbers x, there is a natural number y such that %", where in "%" no further quantifiers appear, there is no difference between ZFC (Zermelo–Fraenkel set theory with the axiom of choice), ZF (set theory without the axiom of choice) and IZF (set theory without the axiom of choice and without the law of excluded middle).
Any ZFC-proof of such a statement can be mechanically transformed to an IZF-proof, with just a modest increase in proof length.
I included some references about this in a set of slides: https://www.speicherleck.de/iblech/stuff/37c3-axiom-of-choic...