Metamath Proof Explorer


Theorem necon1bd

Description: Contrapositive deduction for inequality. (Contributed by NM, 21-Mar-2007) (Proof shortened by Andrew Salmon, 25-May-2011) (Proof shortened by Wolf Lammen, 23-Nov-2019)

Ref Expression
Hypothesis necon1bd.1 φ A B ψ
Assertion necon1bd φ ¬ ψ A = B

Proof

Step Hyp Ref Expression
1 necon1bd.1 φ A B ψ
2 df-ne A B ¬ A = B
3 2 1 syl5bir φ ¬ A = B ψ
4 3 con1d φ ¬ ψ A = B