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


Ref 
Expression 

Hypotheses 
neeqtrr.1 
$${\u22a2}{A}\ne {B}$$ 


neeqtrr.2 
$${\u22a2}{C}={B}$$ 

Assertion 
neeqtrri 
$${\u22a2}{A}\ne {C}$$ 
Proof
Step 
Hyp 
Ref 
Expression 
1 

neeqtrr.1 
$${\u22a2}{A}\ne {B}$$ 
2 

neeqtrr.2 
$${\u22a2}{C}={B}$$ 
3 
2

eqcomi 
$${\u22a2}{B}={C}$$ 
4 
1 3

neeqtri 
$${\u22a2}{A}\ne {C}$$ 