This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	⊢ 𝜑
	mptnan.maj	⊢ ¬ ( 𝜑 ∧ 𝜓 )
Assertion	mptnan	⊢ ¬ 𝜓

Proof

Step	Hyp	Ref	Expression
1		mptnan.min	⊢ 𝜑
2		mptnan.maj	⊢ ¬ ( 𝜑 ∧ 𝜓 )
3	2	imnani	⊢ ( 𝜑 → ¬ 𝜓 )
4	1 3	ax-mp	⊢ ¬ 𝜓