I don't understand why we can use things as the contrapositive, reductio, etc. when we look to prove some statement.
If we look at this from something like axiomatic propositional logic we can say that $$ (p\implies q)\implies(\neg q \implies\neg p) $$ and $$ (\neg q \implies \neg p) \implies(p\implies q) $$
Are theorems, but only if we have the necessary axioms/rules of inference, what happens if we don't?
If we interpret this formulas semantically, on the other hand, its obvious that both formulas are tautologies. And similar argument goes for proofs by contradiction.
So, from this, I gather that when we normally look to prove an implication in mathematics, we follow the rules that semantic propositional logic dictate, why do we accept this?
Somehow related: What the Tortoise said to Achilles.
For me, a convincing argument is already included in your question:
My interest in logic is (most of the time) semantics driven: I have some notion of "structure" or "truth assignment" I'm already interested in, and then I try to understand what the corresponding logic is. Individual axioms/inference rules are justified one by one, and the appropriate completeness theorem tells me when I'm "done".
Of course, the dual of this attitude is equally true of me: that, to the extent that (say) I'm interested in sheaves of first-order structures, then I'm using intuitionistic logic. And this attitude is irrelevant if I'm interested in some formal system for its own sake (e.g. linear logic looks pretty cool, regardless of its semantics). But if you ask my what logic is my "default," for me that's the same as asking what semantics is my "default".
There is a certain circularity here - how do I understand a semantic framework without a logic underpinning my thoughts, already? - but this is part of the point of the Tortoise and Achilles parable: we have to start somewhere.