Metamath Proof Explorer
Description: Inference for inequality. (Contributed by NM, 29Apr2005) (Proof
shortened by Wolf Lammen, 19Nov2019)


Ref 
Expression 

Hypothesis 
neeq1i.1 
$${\u22a2}{A}={B}$$ 

Assertion 
neeq1i 
$${\u22a2}{A}\ne {C}\leftrightarrow {B}\ne {C}$$ 
Proof
Step 
Hyp 
Ref 
Expression 
1 

neeq1i.1 
$${\u22a2}{A}={B}$$ 
2 
1

eqeq1i 
$${\u22a2}{A}={C}\leftrightarrow {B}={C}$$ 
3 
2

necon3bii 
$${\u22a2}{A}\ne {C}\leftrightarrow {B}\ne {C}$$ 