Metamath Proof Explorer


Theorem necon4bid

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

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

Proof

Step Hyp Ref Expression
1 necon4bid.1 φ A B C D
2 1 necon2bbid φ C = D ¬ A B
3 nne ¬ A B A = B
4 2 3 bitr2di φ A = B C = D