Metamath Proof Explorer


Theorem pm2.61ine

Description: Inference eliminating an inequality in an antecedent. (Contributed by NM, 16-Jan-2007) (Proof shortened by Andrew Salmon, 25-May-2011)

Ref Expression
Hypotheses pm2.61ine.1 ( 𝐴 = 𝐵𝜑 )
pm2.61ine.2 ( 𝐴𝐵𝜑 )
Assertion pm2.61ine 𝜑

Proof

Step Hyp Ref Expression
1 pm2.61ine.1 ( 𝐴 = 𝐵𝜑 )
2 pm2.61ine.2 ( 𝐴𝐵𝜑 )
3 nne ( ¬ 𝐴𝐵𝐴 = 𝐵 )
4 3 1 sylbi ( ¬ 𝐴𝐵𝜑 )
5 2 4 pm2.61i 𝜑