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	$$⊢\phi \leftrightarrow \top$$
	aifftbifffaibif.2	$$⊢\psi \leftrightarrow \perp$$
Assertion	aifftbifffaibif	$$⊢\left(\phi \to \psi \right)\leftrightarrow \perp$$

Proof

Step	Hyp	Ref	Expression
1		aifftbifffaibif.1	$$⊢\phi \leftrightarrow \top$$
2		aifftbifffaibif.2	$$⊢\psi \leftrightarrow \perp$$
3	1	aistia	$$⊢\phi$$
4	2	aisfina	$$⊢\neg \psi$$
5	3 4	pm3.2i	$$⊢\left(\phi \wedge \neg \psi \right)$$
6		annim	$$⊢\left(\phi \wedge \neg \psi \right)\leftrightarrow \neg \left(\phi \to \psi \right)$$
7	6	biimpi	$$⊢\left(\phi \wedge \neg \psi \right)\to \neg \left(\phi \to \psi \right)$$
8	5 7	ax-mp	$$⊢\neg \left(\phi \to \psi \right)$$
9	8	bifal	$$⊢\left(\phi \to \psi \right)\leftrightarrow \perp$$