Metamath Proof Explorer
Description: A chained equality inference for inequality. (Contributed by NM, 6Jun2012) (Proof shortened by Wolf Lammen, 19Nov2019)


Ref 
Expression 

Hypotheses 
eqnetrrid.1 
 B = A 


eqnetrrid.2 
 ( ph > B =/= C ) 

Assertion 
eqnetrrid 
 ( ph > A =/= C ) 
Proof
Step 
Hyp 
Ref 
Expression 
1 

eqnetrrid.1 
 B = A 
2 

eqnetrrid.2 
 ( ph > B =/= C ) 
3 
1

a1i 
 ( ph > B = A ) 
4 
3 2

eqnetrrd 
 ( ph > A =/= C ) 