Metamath Proof Explorer


Theorem pm2.61ne

Description: Deduction eliminating an inequality in an antecedent. (Contributed by NM, 24-May-2006) (Proof shortened by Andrew Salmon, 25-May-2011) (Proof shortened by Wolf Lammen, 25-Nov-2019)

Ref Expression
Hypotheses pm2.61ne.1 A = B ψ χ
pm2.61ne.2 φ A B ψ
pm2.61ne.3 φ χ
Assertion pm2.61ne φ ψ

Proof

Step Hyp Ref Expression
1 pm2.61ne.1 A = B ψ χ
2 pm2.61ne.2 φ A B ψ
3 pm2.61ne.3 φ χ
4 3 1 syl5ibr A = B φ ψ
5 2 expcom A B φ ψ
6 4 5 pm2.61ine φ ψ