Metamath Proof Explorer


Theorem necon4bid

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

Ref Expression
Hypothesis necon4bid.1 ( 𝜑 → ( 𝐴𝐵𝐶𝐷 ) )
Assertion necon4bid ( 𝜑 → ( 𝐴 = 𝐵𝐶 = 𝐷 ) )

Proof

Step Hyp Ref Expression
1 necon4bid.1 ( 𝜑 → ( 𝐴𝐵𝐶𝐷 ) )
2 1 necon2bbid ( 𝜑 → ( 𝐶 = 𝐷 ↔ ¬ 𝐴𝐵 ) )
3 nne ( ¬ 𝐴𝐵𝐴 = 𝐵 )
4 2 3 bitr2di ( 𝜑 → ( 𝐴 = 𝐵𝐶 = 𝐷 ) )