Name for Logical Principle $(\varphi \to \psi) \to ((\neg \varphi \to \psi) \to \psi)$ The formula in the title seems like a pretty elementary logic principle.
In terms of an inference, it would be like a Constructive Dilemma:
$P \lor Q$
$P \to R$
$Q \to S$
$\therefore R \lor S$
where we set $Q$ to $\neg P$ and $S$ to $R$:
$P \lor \neg P$
$P \to R$
$Q \to R$
$\therefore R \lor R$  (which of course is just $R$)
and so if we assume of the law of Excluded Middle, we get:
$P \to R$
$\neg P \to R$
$\therefore R$
Does this inference have a name?
I note that if we rewrite the conditionals as disjunctions, it is related to $(P \lor R) \land (\neg P \lor R)$ which by Adjacency is equivalent to $R$ ... but I am thinking there must be some name used for the conditional form of this ... some special kind of 'Dilemma'.
 A: The given proposition bears a kinship to the argument schema historically known as consequentia mirabilis, expressed in propositional form as
$$(\neg\psi\rightarrow\psi)\rightarrow\psi$$
A nice example (also, possibly the first on record) of consequentia mirabilis is  an argument set forth in a fragment from Aristotle (as translated by William Kneale in his article Aristotle and the Consequentia Mirabilis):

If we ought to philosophise, then we ought to philosophise; and if we
ought not to philosophise, then we ought to philosophise (i.e. in
order to justify this view); in any case, therefore, we ought to
philosophise.

We may notice that Descartes's hallmark statement, "I think, therefore I am", also exemplifies consequentia mirabilis. One cannot deny statement in a way that is not self-defeating. As Descartes's case suggests, consequentia mirabilis is intimately connected to our understanding of certainty and our rock-bottom presuppositions.
Consequentia mirabilis tells us that if a proposition $\psi$ is so strong that even its own negation concedes it, then it is true. From this perspective, we can construe the proposition $(\varphi\rightarrow\psi)\rightarrow ((\neg\varphi\rightarrow\psi)\rightarrow\psi)$ as a generalisation from self-referring to referring to any proposition $\varphi$ (including itself). We can explicate this view by comparing them in deductive form as
$$[\psi\rightarrow\psi],\;\neg\psi\rightarrow\psi\vdash\psi$$
and
$$\varphi\rightarrow\psi,\;\neg\varphi\rightarrow\psi\vdash\psi$$
Hence, if we wish to name it, the proposition in question might be called generalised consequentia mirabilis, for it can be said to be so at least in spirit, if not in letter.
