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