Metamath Proof Explorer


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 ( ( ¬ 𝜑𝜑 ) ↔ ⊥ )