This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )