Metamath Proof Explorer

Theorem necon2abii

Description: Contrapositive inference for inequality. (Contributed by NM, 2-Mar-2007)

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

Proof

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