Metamath Proof Explorer

Theorem necon3bii

Description: Inference from equality to inequality. (Contributed by NM, 23-Feb-2005)

Ref Expression
Hypothesis necon3bii.1 
|- ( A = B <-> C = D )
Assertion necon3bii 
|- ( A =/= B <-> C =/= D )

Proof

Step Hyp Ref Expression
1 necon3bii.1 
 |-  ( A = B <-> C = D )
2 1 necon3abii 
 |-  ( A =/= B <-> -. C = D )
3 df-ne 
 |-  ( C =/= D <-> -. C = D )
4 2 3 bitr4i 
 |-  ( A =/= B <-> C =/= D )