Theorem aibnbaif

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

	Ref	Expression
Hypotheses	aibnbaif.1	$$⊢\phi \to \psi$$
	aibnbaif.2	$$⊢\neg \psi$$
Assertion	aibnbaif	$$⊢\phi \leftrightarrow \perp$$

Proof

Step	Hyp	Ref	Expression
1		aibnbaif.1	$$⊢\phi \to \psi$$
2		aibnbaif.2	$$⊢\neg \psi$$
3	1 2	aibnbna	$$⊢\neg \phi$$
4	3	bifal	$$⊢\phi \leftrightarrow \perp$$