Metamath Proof Explorer

Theorem nebi

Description: Contraposition law for inequality. (Contributed by NM, 28-Dec-2008)

Ref Expression
Assertion nebi ⊢A=B↔C=D↔A≠B↔C≠D

Proof

Step Hyp Ref Expression
1 id ⊢A=B↔C=D→A=B↔C=D
2 1 necon3bid ⊢A=B↔C=D→A≠B↔C≠D
3 id ⊢A≠B↔C≠D→A≠B↔C≠D
4 3 necon4bid ⊢A≠B↔C≠D→A=B↔C=D
5 2 4 impbii ⊢A=B↔C=D↔A≠B↔C≠D