First of all, I should have written "recursively enumerable theory" or "theory with decidable axioms". But I think it's clear that I'm referring to things like ZFC, first-order PA or any other similar system.

With that out of the way, it's pretty easy to write a general theorem prover for such theories if you can solve the halting problem.

First define a TM G that takes as input 1. the description of another TM A that decides whether a particular sentence is an axiom of some theory T and 2. a sentence P. We enumerate all syntactically valid proofs with P as the conclusion and check whether all axioms are valid according to A and all inferences are sound. If we find a valid proof, we stop. (G can obviously be built.)

Then define H such that it takes the same inputs as G, and then (using the halting oracle) determines whether G would halt given A and P. If yes, return true, otherwise false.

Then H would be a decider for the language consisting of all pairs T |= P, where T is some recursively enumerable theory.