Metamath Proof Explorer


Theorem necon3bd

Description: Contrapositive law deduction for inequality. (Contributed by NM, 2-Apr-2007) (Proof shortened by Andrew Salmon, 25-May-2011)

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

Proof

Step Hyp Ref Expression
1 necon3bd.1 φ A = B ψ
2 nne ¬ A B A = B
3 2 1 syl5bi φ ¬ A B ψ
4 3 con1d φ ¬ ψ A B