Metamath Proof Explorer


Theorem necon3ad

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

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

Proof

Step Hyp Ref Expression
1 necon3ad.1 φ ψ A = B
2 neneq A B ¬ A = B
3 1 2 nsyli φ A B ¬ ψ