Theorem bicontr

Description: Biconditional of its own negation is a contradiction. (Contributed by Giovanni Mascellani, 15-Sep-2017)

	Ref	Expression
Assertion	bicontr	$$⊢\left(\neg \phi \leftrightarrow \phi \right)\leftrightarrow \perp$$

Proof

Step	Hyp	Ref	Expression
1		biid	$$⊢\phi \leftrightarrow \phi$$
2		notbinot1	$$⊢\neg \left(\neg \phi \leftrightarrow \phi \right)\leftrightarrow \left(\phi \leftrightarrow \phi \right)$$
3	1 2	mpbir	$$⊢\neg \left(\neg \phi \leftrightarrow \phi \right)$$
4	3	bifal	$$⊢\left(\neg \phi \leftrightarrow \phi \right)\leftrightarrow \perp$$