Theorem mptnan

Modus ponendo tollens 1, one of the "indemonstrables" in Stoic logic. See rule 1 on [Lopez-Astorga] p. 12 , rule 1 on [Sanford] p. 40, and rule A3 in [Hitchcock] p. 5. Sanford describes this rule second (after mptxor) as a "safer, and these days much more common" version of modus ponendo tollens because it avoids confusion between inclusive-or and exclusive-or. (Contributed by David A. Wheeler, 3-Jul-2016.)

Hypotheses
mptnan.min
\( \vdash \varphi \)
mptnan.maj
\( \vdash \neg (\varphi \wedge \psi) \)
Conclusion
\( \vdash \neg \psi \)
Proof
l0
mptnan.min
\( \vdash \varphi \)
mptnan.maj
imnani _
\( \vdash \varphi \rightarrow \neg \psi \)
ax-mp l0 _