There is no proof that the axiom is true.
There is no proof by “Proof by contradiction”.
That means that even if you deny the axiom, there will be no contradiction.
And if a contradiction is created by denying the axiom, there is a proof that the axiom is true, so this violates the definition of the axiom, which is "accepted as true without proof," and the axiom is no longer an axiom.
It's a little more complicated than that. But you are starting to ask some good questions about the axiomatic method of reasoning. Let's clarify some ideas.
Today, we use formal systems to reason deductively quite frequently. In fact, there are now logical frameworks that provide a mechanism for choosing all sorts of axioms at the first-order and higher-order by allowing us to treat logical systems as first-class objects in our computations. So, understanding how we choose axioms and what that means to reasoning is very important.
When we build a system of reasoning, we indeed must choose axioms. One of the most famous choices of axioms in the history of logic and mathematics is the parallel postulate of Euclid's axiomatic method is elements. For a couple of thousand years, there was widespread belief both that the axiom might be reducible to the other axioms and that the interpretation of the axiom was immutable. Of course, the end to all of this attention was the realization that it was not reducible, but that there were parallel interpretations. The product were various non-Euclidean geometries.
In reverse mathematics, we often find ourselves searching for new axioms. Often times, we can show using mathematical logic that something cannot be proved with the current set of axioms. Thus, a search for a new axiom to arrive at a sure conclusion from or about the system drive the adoption of a new axiom. The transition of ZF to ZFC exemplifies this happening.
But what you're asking about is weakening a system of logic by rejecting or removing an axiom by presuming it's not true. A historical example of this is the development of intuition logic (IL) from classical logic by rejecting an axiom. IL rejects not one, but two axioms, LEM and DN.
So, when you reject an axiom, you change your system of logic which is usually just phrased as 'having a different logic'. There are all sorts of logics and the interesting one's are the non-classical ones. Click on Bumble's response to 'In how many and which ways can a logic be non-classical? Are there systems for organizing them?' (PhilSE) for more information.
Now, interestingly, one axiom in reasoning that you can reject is law of non-contradiction. Another is the principle of bivalence. From WP:
In logic, the semantic principle (or law) of bivalence states that every declarative sentence expressing a proposition (of a theory under inspection) has exactly one truth value, either true or false. A logic satisfying this principle is called a two-valued logic or bivalent logic.
So, when you start rejecting axioms in a formal system, you can indeed wind up with issues regarding contradictions and tautologies, and whether or not the system of logic is even useful becomes a question. Famously, changing your logic system can result in occurrences of the principle of explosion or other related outcomes. In fact, there is a class of logics where contradiction is even allowed, those are the paraconsistent logics.
I'm going to respond a second time because your modification to your original question seemed to me to present a wider discussion about using axiomatic reasoning to practical ends.
You said:
And if a contradiction is created by denying the axiom, there is a proof that the axiom is true, so this violates the definition of the axiom, which is "accepted as true without proof," and the axiom is no longer an axiom.
Yes. In the context of argumentation, this is the fundamental nature of reductio ad absurdum. From WP:
form of argument that attempts to establish a claim by showing that the opposite scenario would lead to absurdity or contradiction.13 This argument form traces back to Ancient Greek philosophy and has been used throughout history in both formal mathematical and philosophical reasoning, as well as in debate. The equivalent formal rule is known as negation introduction. A related mathematical proof technique is called proof by contradiction.
One simple use of this is to assume there are a finite number of natural numbers which leads us to the conclusion there is some largest natural number n. But, for any n, we are allowed to add 1 according to the rules of arithmetic. Thus, for any largest number n, there is always an n+1. Therefore, given the contradiction there is always a bigger number, our axiom that there are a finite number of natural numbers must be false, and we can reject the claim. That's why it is axiomatic that the naturals are an infinite set.
Another classic example is the proof there is an infinite number of primes. We assume there isn't (an axiom), and then we construct a composite as a sequence of products of primes and add one. The result is that when we presume that there are not an infinite number of primes, we wind up with a construction of a new prime that is larger than our prime construction, and therefore, like in our first example, there must be an infinite number of primes. That is why it is axiomatic primes are an infinite set.
In the olden days, self-evidential was presumed to be the same to everyone, but modern philosophy of science now concedes, that self-evidential is no easy task with some parties accepting that self-evidential is undermined by theory-ladenness. What should be noted that "accepted as true without proof" is vague language. What 'true' means and what 'proof' means is a question for epistemology, particularly in theories of truth-conditional semantics and evidentialism more specifically. So, yes, we often adopt an axiom, reason through deductive inferences to a contradiction, and then decide the axiom must be false.
A positive version of this problem was addressed in A "paradox" of foundationalism? here on the PhilosophySE. The issue was that if we start from the problem of infinite regresses of knowledge, and use the existence of said problem as a premise, combined with premises about attempts at positive solutions, and then conclude with foundationalism, we seem to be deducing that there are non-deductive stages of reasoning, which seems ironic even if it doesn't quite defeat the point of foundationalism as such (see e.g. Adam Sharpe's answer to my question, there).
Now in the set theories of large cardinals, there is this phenomenon where we deduce that such-and-such a proposition would be an axiom relative to other possible axioms, but yet all these would-be starting points of reasoning turn out to be deducible modulo some other would-be starting points, and of the kingdom of this "madness" there seems to be no end. Hamkins[22] and [12] are especially perspicuous discussions of such a situation; moreover, in fact, it is easy to imagine a system of large cardinals that starts out as if it were strictly well-founded but once generalized on its own terms transmutes into an inverse pattern of principles (for the details, see my answer to yet another question on this SE).
