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	|- ( ph -> ps )
	aibnbaif.2	|- -. ps
Assertion	aibnbaif	|- ( ph <-> F. )

Proof

Step	Hyp	Ref	Expression
1		aibnbaif.1	|- ( ph -> ps )
2		aibnbaif.2	|- -. ps
3	1 2	aibnbna	|- -. ph
4	3	bifal	|- ( ph <-> F. )