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


Ref 
Expression 

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


3netr3d.2 
 ( ph > A = C ) 


3netr3d.3 
 ( ph > B = D ) 

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

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

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

3netr3d.3 
 ( ph > B = D ) 
4 
1 3

neeqtrd 
 ( ph > A =/= D ) 
5 
2 4

eqnetrrd 
 ( ph > C =/= D ) 