Metamath Proof Explorer
Description: Substitution of equality into both sides of an inequality. (Contributed by NM, 24Jul2012) (Proof shortened by Wolf Lammen, 21Nov2019)


Ref 
Expression 

Hypotheses 
3netr4d.1 
 ( ph > A =/= B ) 


3netr4d.2 
 ( ph > C = A ) 


3netr4d.3 
 ( ph > D = B ) 

Assertion 
3netr4d 
 ( ph > C =/= D ) 
Proof
Step 
Hyp 
Ref 
Expression 
1 

3netr4d.1 
 ( ph > A =/= B ) 
2 

3netr4d.2 
 ( ph > C = A ) 
3 

3netr4d.3 
 ( ph > D = B ) 
4 
2 1

eqnetrd 
 ( ph > C =/= B ) 
5 
4 3

neeqtrrd 
 ( ph > C =/= D ) 