Metamath Proof Explorer


Theorem necon2abid

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

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

Proof

Step Hyp Ref Expression
1 necon2abid.1 ( 𝜑 → ( 𝐴 = 𝐵 ↔ ¬ 𝜓 ) )
2 notnotb ( 𝜓 ↔ ¬ ¬ 𝜓 )
3 1 necon3abid ( 𝜑 → ( 𝐴𝐵 ↔ ¬ ¬ 𝜓 ) )
4 2 3 bitr4id ( 𝜑 → ( 𝜓𝐴𝐵 ) )