Metamath Proof Explorer
Description: Inference eliminating an inequality in an antecedent. (Contributed by NM, 16Jan2007) (Proof shortened by Andrew Salmon, 25May2011)


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 
⊢ 𝜑 