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	⊢ ( 𝜑 ↔ ⊤ )
	aifftbifffaibifff.2	⊢ ( 𝜓 ↔ ⊥ )
Assertion	aifftbifffaibifff	⊢ ( ( 𝜑 ↔ 𝜓 ) ↔ ⊥ )

Proof

Step	Hyp	Ref	Expression
1		aifftbifffaibifff.1	⊢ ( 𝜑 ↔ ⊤ )
2		aifftbifffaibifff.2	⊢ ( 𝜓 ↔ ⊥ )
3	1	aistia	⊢ 𝜑
4	2	aisfina	⊢ ¬ 𝜓
5	3 4	abnotbtaxb	⊢ ( 𝜑 ⊻ 𝜓 )
6	5	axorbtnotaiffb	⊢ ¬ ( 𝜑 ↔ 𝜓 )
7		nbfal	⊢ ( ¬ ( 𝜑 ↔ 𝜓 ) ↔ ( ( 𝜑 ↔ 𝜓 ) ↔ ⊥ ) )
8	7	biimpi	⊢ ( ¬ ( 𝜑 ↔ 𝜓 ) → ( ( 𝜑 ↔ 𝜓 ) ↔ ⊥ ) )
9	6 8	ax-mp	⊢ ( ( 𝜑 ↔ 𝜓 ) ↔ ⊥ )