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	|- ph
	mptnan.maj	|- -. ( ph /\ ps )
Assertion	mptnan	|- -. ps

Proof

Step	Hyp	Ref	Expression
1		mptnan.min	|- ph
2		mptnan.maj	|- -. ( ph /\ ps )
3	2	imnani	|- ( ph -> -. ps )
4	1 3	ax-mp	|- -. ps