Metamath Proof Explorer
Description: Inference from commutative law for inequality. (Contributed by NM, 17Oct2012)


Ref 
Expression 

Hypothesis 
necomi.1 
$${\u22a2}{A}\ne {B}$$ 

Assertion 
necomi 
$${\u22a2}{B}\ne {A}$$ 
Proof
Step 
Hyp 
Ref 
Expression 
1 

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

necom 
$${\u22a2}{A}\ne {B}\leftrightarrow {B}\ne {A}$$ 
3 
1 2

mpbi 
$${\u22a2}{B}\ne {A}$$ 