Theorem aifftbifffaibif

Description: Given a is equivalent to T., Given b is equivalent to F., there exists a proof for that a implies b is false. (Contributed by Jarvin Udandy, 7-Sep-2020)

	Ref	Expression
Hypotheses	aifftbifffaibif.1	|- ( ph <-> T. )
	aifftbifffaibif.2	|- ( ps <-> F. )
Assertion	aifftbifffaibif	|- ( ( ph -> ps ) <-> F. )

Proof

Step	Hyp	Ref	Expression
1		aifftbifffaibif.1	|- ( ph <-> T. )
2		aifftbifffaibif.2	|- ( ps <-> F. )
3	1	aistia	|- ph
4	2	aisfina	|- -. ps
5	3 4	pm3.2i	|- ( ph /\ -. ps )
6		annim	|- ( ( ph /\ -. ps ) <-> -. ( ph -> ps ) )
7	6	biimpi	|- ( ( ph /\ -. ps ) -> -. ( ph -> ps ) )
8	5 7	ax-mp	|- -. ( ph -> ps )
9	8	bifal	|- ( ( ph -> ps ) <-> F. )