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 
|- ( ( -. ph <-> ph ) <-> F. )

Proof

Step Hyp Ref Expression
1 biid 
 |-  ( ph <-> ph )
2 notbinot1 
 |-  ( -. ( -. ph <-> ph ) <-> ( ph <-> ph ) )
3 1 2 mpbir 
 |-  -. ( -. ph <-> ph )
4 3 bifal 
 |-  ( ( -. ph <-> ph ) <-> F. )