Theorem aifftbifffaibifff

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

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

Proof

Step	Hyp	Ref	Expression
1		aifftbifffaibifff.1	|- ( ph <-> T. )
2		aifftbifffaibifff.2	|- ( ps <-> F. )
3	1	aistia	|- ph
4	2	aisfina	|- -. ps
5	3 4	abnotbtaxb	|- ( ph \/_ ps )
6	5	axorbtnotaiffb	|- -. ( ph <-> ps )
7		nbfal	|- ( -. ( ph <-> ps ) <-> ( ( ph <-> ps ) <-> F. ) )
8	7	biimpi	|- ( -. ( ph <-> ps ) -> ( ( ph <-> ps ) <-> F. ) )
9	6 8	ax-mp	|- ( ( ph <-> ps ) <-> F. )