Consistency of a negated-consistency extension ($S⊢{\mathrm{Con}}_S\to {\mathrm{Con}}_{S+\neg {\mathrm{Con}}_S}$)

For adequate arithmetic provability predicates, the arithmetized deduction theorem identifies inconsistency of $S+\neg {\mathrm{Con}}_S$ with $S$-provability of ${\mathrm{Con}}_S$. Formalized second incompleteness gives ${\square }_S{\mathrm{Con}}_S\to {\square }_S\perp$. Contraposition yields the displayed conditional. This is an internal theorem and does not license removal of its consistency premise.