Metamath Proof Explorer
Description: An inference from an inequality, related to modus tollens. (Contributed by NM, 13Apr2007)


Ref 
Expression 

Hypotheses 
nemtbir.1 
 A =/= B 


nemtbir.2 
 ( ph <> A = B ) 

Assertion 
nemtbir 
 . ph 
Proof
Step 
Hyp 
Ref 
Expression 
1 

nemtbir.1 
 A =/= B 
2 

nemtbir.2 
 ( ph <> A = B ) 
3 
1

neii 
 . A = B 
4 
3 2

mtbir 
 . ph 