Metamath Proof Explorer

Theorem necon3bbii

Description: Deduction from equality to inequality. (Contributed by NM, 13-Apr-2007)

Ref Expression
Hypothesis necon3bbii.1 
|- ( ph <-> A = B )
Assertion necon3bbii 
|- ( -. ph <-> A =/= B )

Proof

Step Hyp Ref Expression
1 necon3bbii.1 
 |-  ( ph <-> A = B )
2 1 bicomi 
 |-  ( A = B <-> ph )
3 2 necon3abii 
 |-  ( A =/= B <-> -. ph )
4 3 bicomi 
 |-  ( -. ph <-> A =/= B )