Metamath Proof Explorer


Theorem necon4bid

Description: Contrapositive law deduction for inequality. (Contributed by NM, 29-Jun-2007)

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

Proof

Step Hyp Ref Expression
1 necon4bid.1
 |-  ( ph -> ( A =/= B <-> C =/= D ) )
2 1 necon2bbid
 |-  ( ph -> ( C = D <-> -. A =/= B ) )
3 nne
 |-  ( -. A =/= B <-> A = B )
4 2 3 bitr2di
 |-  ( ph -> ( A = B <-> C = D ) )