Metamath Proof Explorer


Theorem necon2bbid

Description: Contrapositive deduction for inequality. (Contributed by NM, 13-Apr-2007) (Proof shortened by Wolf Lammen, 24-Nov-2019)

Ref Expression
Hypothesis necon2bbid.1 ( 𝜑 → ( 𝜓𝐴𝐵 ) )
Assertion necon2bbid ( 𝜑 → ( 𝐴 = 𝐵 ↔ ¬ 𝜓 ) )

Proof

Step Hyp Ref Expression
1 necon2bbid.1 ( 𝜑 → ( 𝜓𝐴𝐵 ) )
2 notnotb ( 𝜓 ↔ ¬ ¬ 𝜓 )
3 1 2 bitr3di ( 𝜑 → ( 𝐴𝐵 ↔ ¬ ¬ 𝜓 ) )
4 3 necon4abid ( 𝜑 → ( 𝐴 = 𝐵 ↔ ¬ 𝜓 ) )