But when you want to combine A and B and start to work in a logic that is the union of their logics you end up doing a proof in a logic that often loses all the

But when you want to combine A and B and start to work in a logic that is the union of their logics you end up doing a proof in a logic that often loses all the nice properties that were essential to the theorem proving being reasonable. This works if combining A and B is the entire proof, but how do you handle searching for good next steps in the new logic that lacks those properties if there are other pieces of the proof to be done still?