Metamath Proof Explorer

Theorem necon2bbii

Description: Contrapositive inference for inequality. (Contributed by NM, 13-Apr-2007)

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

Proof

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