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	$$⊢\phi \to \psi$$
	aibnbna.2	$$⊢\neg \psi$$
Assertion	aibnbna	$$⊢\neg \phi$$

Proof

Step	Hyp	Ref	Expression
1		aibnbna.1	$$⊢\phi \to \psi$$
2		aibnbna.2	$$⊢\neg \psi$$
3	2 1	mto	$$⊢\neg \phi$$