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	⊢ ( 𝜑 → 𝜓 )
	aibnbaif.2	⊢ ¬ 𝜓
Assertion	aibnbaif	⊢ ( 𝜑 ↔ ⊥ )

Proof

Step	Hyp	Ref	Expression
1		aibnbaif.1	⊢ ( 𝜑 → 𝜓 )
2		aibnbaif.2	⊢ ¬ 𝜓
3	1 2	aibnbna	⊢ ¬ 𝜑
4	3	bifal	⊢ ( 𝜑 ↔ ⊥ )