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

Proof

Step	Hyp	Ref	Expression
1		aifftbifffaibif.1	⊢ ( 𝜑 ↔ ⊤ )
2		aifftbifffaibif.2	⊢ ( 𝜓 ↔ ⊥ )
3	1	aistia	⊢ 𝜑
4	2	aisfina	⊢ ¬ 𝜓
5	3 4	pm3.2i	⊢ ( 𝜑 ∧ ¬ 𝜓 )
6		annim	⊢ ( ( 𝜑 ∧ ¬ 𝜓 ) ↔ ¬ ( 𝜑 → 𝜓 ) )
7	6	biimpi	⊢ ( ( 𝜑 ∧ ¬ 𝜓 ) → ¬ ( 𝜑 → 𝜓 ) )
8	5 7	ax-mp	⊢ ¬ ( 𝜑 → 𝜓 )
9	8	bifal	⊢ ( ( 𝜑 → 𝜓 ) ↔ ⊥ )