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 ¬ φ φ