Theorem bicontr

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

	Ref	Expression
Assertion	bicontr	⊢ ( ( ¬ 𝜑 ↔ 𝜑 ) ↔ ⊥ )

Proof

Step	Hyp	Ref	Expression
1		biid	⊢ ( 𝜑 ↔ 𝜑 )
2		notbinot1	⊢ ( ¬ ( ¬ 𝜑 ↔ 𝜑 ) ↔ ( 𝜑 ↔ 𝜑 ) )
3	1 2	mpbir	⊢ ¬ ( ¬ 𝜑 ↔ 𝜑 )
4	3	bifal	⊢ ( ( ¬ 𝜑 ↔ 𝜑 ) ↔ ⊥ )