Theorem mptnan

Description: 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)

	Ref	Expression
Hypotheses	mptnan.min	$$⊢\phi$$
	mptnan.maj	$$⊢\neg \left(\phi \wedge \psi \right)$$
Assertion	mptnan	$$⊢\neg \psi$$

Proof

Step	Hyp	Ref	Expression
1		mptnan.min	$$⊢\phi$$
2		mptnan.maj	$$⊢\neg \left(\phi \wedge \psi \right)$$
3	2	imnani	$$⊢\phi \to \neg \psi$$
4	1 3	ax-mp	$$⊢\neg \psi$$