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 φ A = B ¬ ψ
Assertion necon2abid φ ψ A B

Proof

Step Hyp Ref Expression
1 necon2abid.1 φ A = B ¬ ψ
2 1 necon3abid φ A B ¬ ¬ ψ
3 notnotb ψ ¬ ¬ ψ
4 2 3 syl6rbbr φ ψ A B