Theorem aibnbna

Description: Given a implies b, (not b), there exists a proof for (not a). (Contributed by Jarvin Udandy, 1-Sep-2016)

	Ref	Expression
Hypotheses	aibnbna.1	⊢ ( 𝜑 → 𝜓 )
	aibnbna.2	⊢ ¬ 𝜓
Assertion	aibnbna	⊢ ¬ 𝜑

Proof

Step	Hyp	Ref	Expression
1		aibnbna.1	⊢ ( 𝜑 → 𝜓 )
2		aibnbna.2	⊢ ¬ 𝜓
3	2 1	mto	⊢ ¬ 𝜑