Metamath Proof Explorer
Description: Substitution of equal classes into an inequality. (Contributed by NM, 4Jul2012)


Ref 
Expression 

Hypotheses 
neeqtrrd.1 
 ( ph > A =/= B ) 


neeqtrrd.2 
 ( ph > C = B ) 

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

neeqtrrd.1 
 ( ph > A =/= B ) 
2 

neeqtrrd.2 
 ( ph > C = B ) 
3 
2

eqcomd 
 ( ph > B = C ) 
4 
1 3

neeqtrd 
 ( ph > A =/= C ) 