Metamath Proof Explorer


Theorem necon3d

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

Ref Expression
Hypothesis necon3d.1 φ A = B C = D
Assertion necon3d φ C D A B

Proof

Step Hyp Ref Expression
1 necon3d.1 φ A = B C = D
2 1 necon3ad φ C D ¬ A = B
3 df-ne A B ¬ A = B
4 2 3 syl6ibr φ C D A B