Metamath Proof Explorer
Description: Deduction eliminating an inequality in an antecedent. (Contributed by NM, 30Nov2011)


Ref 
Expression 

Hypotheses 
pm2.61dane.1 
⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → 𝜓 ) 


pm2.61dane.2 
⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → 𝜓 ) 

Assertion 
pm2.61dane 
⊢ ( 𝜑 → 𝜓 ) 
Proof
Step 
Hyp 
Ref 
Expression 
1 

pm2.61dane.1 
⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → 𝜓 ) 
2 

pm2.61dane.2 
⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → 𝜓 ) 
3 
1

ex 
⊢ ( 𝜑 → ( 𝐴 = 𝐵 → 𝜓 ) ) 
4 
2

ex 
⊢ ( 𝜑 → ( 𝐴 ≠ 𝐵 → 𝜓 ) ) 
5 
3 4

pm2.61dne 
⊢ ( 𝜑 → 𝜓 ) 