Theorem mptxor

Modus ponendo tollens 2, one of the "indemonstrables" in Stoic logic. Note that this uses exclusive-or \/_. See rule 2 on [Lopez-Astorga] p. 12 , rule 4 on [Sanford] p. 39 and rule A4 in [Hitchcock] p. 5 . (Contributed by David A. Wheeler, 3-Jul-2016.) (Proof shortened by Wolf Lammen, 12-Nov-2017.) (Proof shortened by BJ, 19-Apr-2019.)

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