Here is the question:
Given that the principle only affects validity, not soundness, I would expect no consequence at all. Is that correct?
To reject the law of explosion means rejecting the law of contradiction. Paraconsistent logics attempt "to deal with contradictions in a discriminating way". They want "to formalize inconsistent but non-trivial theories". In classical logic a single inconsistency in a theory implies that the theory is trivial since every sentence of the theory is a theorem.
However, Wikipedia notes that there are consequences when comparing these logics with classical logic:
Paraconsistent logics are propositionally weaker than classical logic; that is, they deem fewer propositional inferences valid. The point is that a paraconsistent logic can never be a propositional extension of classical logic, that is, propositionally validate everything that classical logic does. In some sense, then, paraconsistent logic is more conservative or cautious than classical logic.
The consequences of rejecting explosion (and hence non-contradiction) result in a logic that is weaker than classical logic although it may be more expressive.
Here is the question after the revision:
Do you know of any mathematical theorem whose proof relies on the use of the principle of explosion (ECQ)?
One could look at theorems that rely on indirect proof (reductio ad absudrum) or which could be viewed as cases that one eliminates. The indirect proof makes an assumption, reaches a contradiction and then rejects the assumption. This can be viewed as a proof by cases using the principle of bivalence: Either the assumption is true or its negation is true.
Here is an example. Prove that there are infinitely many primes.
For the indirect proof approach, assume there are finitely many primes and let N be the largest prime. Multiply all of the finitely many primes together and add 1 to it. That number is either prime or it contains a prime divisor larger than N. That contradicts the assumption that N is the largest prime and so the assumption is rejected.
To see this as a proof by cases where explosion is used claim that either there is a largest prime or there is not a largest prime. Consider the case when there is a largest prime. Use the method above to reach a contradiction. Use explosion to get any result one wants. Choose the result that there is no largest prime. Now in both cases one gets the same result. Use disjunction elimination to conclude there is no largest prime.
Wikipedia contributors. (2019, April 6). Paraconsistent logic. In Wikipedia, The Free Encyclopedia. Retrieved 15:44, May 1, 2019, from https://en.wikipedia.org/w/index.php?title=Paraconsistent_logic&oldid=891268995