You could (presumably) construct axiom systems under which this is not true, and I believe that some logicians do this sort of thing, but this is rather far removed from mainstream research mathematics.
The Banach-Tarski paradox comes to mind first. I don't think anyone argues that the proof is wrong, but you'll easily find people to argue that that very fact means that the full axiom of choice should be held in deep suspicion.
The 4-color map coloring theorem is more interesting in this thread, though; I think it's the best known example of a proof that offers little to no insight into why the theorem is true. I don't think any solution that requires breaking a problem into 1,936 special cases, and then mechanically checking each one of those cases, will ever lead to an understanding that makes the theorem "obvious".
Looking for insight is what many people do in mathematics, but nonetheless believing that every true fact is true for a reason is naive, just as naive as believing that every problem has to have a solution. So far, most of the time we succeed in explaining why true things are true, but it may be the case that some facts are true merely by combinatorics, and not for human-imaginable reason.
Sure, I would like to believe that there is a crucial observation we haven't made yet that makes 4 color theorem easy, just as it is for 6 color theorem. Nevertheless, I accept the fact that there may be no such thing and 4 color theorem holds just because the constraints force it to be.
I remember reading something of Chaitin's a couple of years ago that drove home the point that most mathematical facts are, in some fairly-well defined sense, true for no reason at all.
(Alas, I don't remember the argument well enough to re-cap it here.)
No, the problem that those who dislike the axiom of choice have is not inherent with the axiom but more the law of excluded middle. Constructivism has no rooms for such imaginings hence those who follow it are not happy with existential proofs. This more practical viewpoint will prove more profound IMHO just as bayesianism is winning the day. Just too many things connected.. types and terms in programs, intuitionistic logic, parts of physics, topoi, CCC.