Metamath Proof Explorer


Theorem pm2.61dne

Description: Deduction eliminating an inequality in an antecedent. (Contributed by NM, 1-Jun-2007) (Proof shortened by Andrew Salmon, 25-May-2011)

Ref Expression
Hypotheses pm2.61dne.1 φ A = B ψ
pm2.61dne.2 φ A B ψ
Assertion pm2.61dne φ ψ

Proof

Step Hyp Ref Expression
1 pm2.61dne.1 φ A = B ψ
2 pm2.61dne.2 φ A B ψ
3 nne ¬ A B A = B
4 3 1 syl5bi φ ¬ A B ψ
5 2 4 pm2.61d φ ψ